Under equivalent typeclasses

Stream: mathlib4

[Aaron Liu]

If we have [CompactSpace X], then [T2Space X] up to [T4Space X] are all equivalent, so which one should be used in a lemma statement?

[Aaron Liu]

More generally, if there are multiple equivalent typeclass combinations that say the same thing, which one should be used in the hypotheses or conclusion of a theorem?

[Jireh Loreaux]

Compact + T2 is a very common assumption mathematically, so it definitely makes sense to use that in this case. More generally, I would say that we generally want to pick a "standard set", and which things are in that standard set is situation-dependent.

[Aaron Liu]

Alright, here's some more combinations I can think of at the moment:

• under [NormalSpace X], [R0Space X] up to [CompletelyRegularSpace X] are equivalent
• under [IsDirected X (· ≤ ·)], [NoMaxOrder X] is equivalent to [NoTopOrder X] (and same for its dual)

[Yury G. Kudryashov]

I think that we should choose R1Space/T2Space whenever there is a bunch of equivalent *Space options.

[Yury G. Kudryashov]

Not sure about NoMaxOrder vs NoTopOrder.