basic facts about Gdelta sets

[affeldt-aist]

Motivation for this change

fyi @mkerjean (application of Baire)

@IshiguroYoshihiro

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• 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

[t6s]

Why not parallelly formalize Fsigma sets too?
(renaming the file to borel_hierarchy.v)

[t6s]

like this affeldt-aist#40

[affeldt-aist]

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.

[affeldt-aist]

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.

[t6s]

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).

[t6s]

Looks good.

[affeldt-aist]

I'll merge tomorrow if the CI is green unless there is new input.