Separation axioms

Stream: maths

[Yury G. Kudryashov]

I suggest that we reformulate (some? most?) separation axioms in terms of filters. E.g.,

• $T_0$ space: inseparable x y implies x = y, see #15046;
• $T_1$ space: leave as is; the equivalent statement "specializes x y implies x = y" is less natural;
• $T_2$ space: if x ≠ y, then their nhds are disjoint;
• $T_{2.5}$ space: if x ≠ y, then "closures" of their nhds are disjoint (needs a new definition filter.map_sets with filter.comap = map_sets preimage)
• regular space: if s is a closed set and x does not belong to this set, then nhds x and set_nhds s are disjoint;
• normal space: if s and t are disjoint closed sets, then set_nhds s and set_nhds t are disjoint.

What do you think?

[Yaël Dillies]

Beware of #14950.