Defining perfect spaces

Stream: mathlib4

[Emilie (Shad Amethyst)]

In my formalization of Rubin's theorem (of which a few PRs are waiting to get reviewed/approved as of writing this), one of the conditions is that the topological space must not have any isolated points. This is equivalent to say that the universe must be a docs#Perfect space.

Looking at the module for Perfect, I see that it contains both elementary properties of perfect sets, and 4 theorems that only apply to metric spaces. So I would like to ask if I could contribute the following changes:

• move the last 4 theorems to a different module, for instance Mathlib.Topology.MetricSpace.Perfect
• move Mathlib.Topology.Perfect up the import chain, so that it only imports Mathlib.Topology.Basic, Mathlib.Topology.Constructions (for the nhdsWithin filter) and Mathlib.Topology.ContinuousOn (which includes nhdsWithin_union, despite it having no reason to be in this file)
• define the PerfectSpace class, which simply states that Perfect Set.univ
• create an instance for [PerfectSpace X] → (x : X) → Filter.NeBot (𝓝[≠] x)
• refactor docs#ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space to instead be an instance of PerfectSpace (the instance will then be provided by the previous bullet, and Mathlib.Topology.Perfect will be high enough in the import chain that it can be imported in Mathlib.Topology.Separation)
• possibly provide an instance for [PerfectSpace X] → [PerfectSpace (X × Y)]
• in another PR, possibly move docs#nhdsWithin_union & co. to Mathlib.Topology.Constructions, since they have no reason to be in ContinuousOn

[Emilie (Shad Amethyst)]

Hmm, actually a few of the theorems require things from Mathlib.Topology.Separation, so the refactor of docs#ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space could possibly be moved to Mathlib.Topology.Perfect instead

[Emilie (Shad Amethyst)]

One small question that I have is that the condition for PerfectSpace (X × Y) only requires X or Y to also be a PerfectSpace, but I'm worried that adding both instances will lead to worse performance in the instance synthetizer

[Sébastien Gouëzel]

I think you can safely add both instances: this should not be on an instance-critical path anyway.

[Antoine Chambert-Loir]

Would it be possible that for the same spaces, the two instances are chosen. If PerfectSpace is a Prop, they would be equal, but are there cases where Lean would be confused anyway?

[Emilie (Shad Amethyst)]

Good call. PerfectSpace is a Prop, but I don't know if this can cause confusion

[Emilie (Shad Amethyst)]

I opened #10246; there seems to be a few places (especially in normed fields and modules) where an ad-hoc ∀ x, Filter.NeBot (𝓝[≠] x) could be replaced with a PerfectSpace instance, but I fear that doing so might slow down the review process even more, and I am running out of PRs that I can concurrently open without making them dependent on one another

[Emilie (Shad Amethyst)]

Antoine Chambert-Loir said:

Would it be possible that for the same spaces, the two instances are chosen. If PerfectSpace is a Prop, they would be equal, but are there cases where Lean would be confused anyway?

Thinking about this, we have a bunch of instances of Nontrivial floating around, and those don't seem to be causing an issue

[Emilie (Shad Amethyst)]

Yay, the split into Mathlib.Topology.MetricSpace.Perfect just got merged!
Right now #10246 is only for defining PerfectSpace; there are quite a few places where it can be used (in PreconnectedSpaces, for proving that spaces or open sets are infinite, and different constructions for PerfectSpace), but I'm keeping these changes for a future PR, since they're kind of expensive to maintain in a dependent PR (with merge conflicts happening now and then, and I need to cherry-pick fixes I make to the dependency PR), and they wouldn't really belong to #10246.

I have a bit of breathing room for the remainder of this week, so I'll also look into moving theorems in ContinuousOn up to Constructions