math-comp
basic facts about Gdelta sets
Motivation for this change
fyi @mkerjean (application of Baire)
@IshiguroYoshihiro
Checklist
- [x] added corresponding entries in
CHANGELOG_UNRELEASED.md
- [x] added corresponding documentation in the headers
Reference: How to document
Merge policy
As a rule of thumb:
- PRs with several commits that make sense individually and that all compile are preferentially merged into master.
- PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers
- Read this Checklist
- Put a milestone if possible
- Check labels
Why not parallelly formalize Fsigma sets too? (renaming the file to borel_hierarchy.v)
Why not parallelly formalize Fsigma sets too? (renaming the file to borel_hierarchy.v)
Why not. We were just trying to keep the PR to a minimal to ease review.
A borel_hierarchy.v file sounds nice.
The last commit moves the definition rational that was lingering into pi_irrational.v into reals.v along with the definition of irrational. It is a bit more principled but a bit longish. There are lemmas about dense in borel_hierarchy.v that should maybe be moved near the definition of dense. The file borel_hierarchy.v is a bit short. Do you have something in mind @t6s ?
By the way, @IshiguroYoshihiro and I wanted to introduce these definitions because they are use in work in progress and since we proved a lemma using Baire and rational that were already in master, we thought it was timely.
It looks short but a nice place for future additions, e.g., a generic definition of the borel hierarchy parametrized by a well-ordered set.
Btw, there will be another demand for this PR from PR #1585 (by @motikaku), where perfect normality is introduced in terms of (sharp) Urysohn functions, but is planned to be related to Gdelta sets (Vedenissoff's theorem).