Changing PerfectSpace

Stream: mathlib4

[Alex Meiburg]

In #35494 I mistakenly used docs#PerfectSpace, but then @Yury G. Kudryashov pointed out that Filter.NeBot (𝓝[≠] x) is preferred. I looked into it and it seems like a bit of a mess.

PerfectSpace is actually used very little. Actually the only instance it's ever used to derive is PerfectSpace.not_isolated (according to loogle).

But I guess there's several places that produce a Filter.NeBot (𝓝[≠] x) instance?

And there are several duplicates then:

• ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space and instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial
• instPerfectSpace and NormedField.nhdsNE_neBot
• perfectSpace_of_module roughly corresponds to both Real.punctured_nhds_module_neBotBasic.html#Module.punctured_nhds_neBot) and Module.punctured_nhds_neBot but neither exactly

And then there are some that aren't duplicated:

• instNeBotNhdsWithinComplSetSingletonOfNontrivial
• OnePoint.nhdsNE_coe_neBot

[Alex Meiburg]

I'd like to propose changing the definition to

abbrev PerfectSpace (X : Type*) [TopologicalSpace X] :=
  ∀ (x : X), Filter.NeBot (𝓝[≠] x)

so that really these are one and the same. The current definition states it in terms of Preperfect Set.univ, and we can make an alternate constructor for that notion then.

Then refactoring all the above to use PerfectSpace as the instance they create/use. Filter.NeBot (𝓝[≠] x) would only be used otherwise for something that only applies to certain points, for instance
OnePoint.nhdsNE_coe_neBot would stay as it is.

[Yury G. Kudryashov]

I think that this refactor should go to a new PR, but #35494 should just state the lemma assuming Filter.NeBot (𝓝[≠] x) for this specific point.

[Yury G. Kudryashov]

In fact, we've discussed introducing a name for this property (e.g., NonIsolatedPt) a few times, but I was too lazy to do it.

[Alex Meiburg]

Oh yes, I agree new PR. I just wanted to ask here before doing such

[Yury G. Kudryashov]

CC: @Eric Wieser AFAIR, you had a related PR.

[Eric Wieser]

Was that docs#NontrivialTopology ?

[Yury G. Kudryashov]

Yes, this one. It's equivalent to PerfectSpace for a TVS over $\mathbb R$, right?

[Aaron Liu]

it's not

[Aaron Liu]

the trivial topology is always PerfectSpace if the type is Nontrivial