Commit 2024-01-29 18:36 7458f0e7

feat(Topology/Separation): define R₁ spaces, review API (#10085)

Main API changes

• Define R1Space, a.k.a. preregular space.
• Drop T2OrLocallyCompactRegularSpace.
• Generalize all existing theorems about T2OrLocallyCompactRegularSpace to R1Space.
• Drop the [T2OrLocallyCompactRegularSpace _] assumption if the space is known to be regular for other reason (e.g., because it's a topological group).

New theorems

• Specializes.not_disjoint: if x ⤳ y, then 𝓝 x and 𝓝 y aren't disjoint;
• specializes_iff_not_disjoint, Specializes.inseparable, disjoint_nhds_nhds_iff_not_inseparable, r1Space_iff_inseparable_or_disjoint_nhds: basic API about R1Spaces;
• Inducing.r1Space, R1Space.induced, R1Space.sInf, R1Space.iInf, R1Space.inf, instances for Subtype _, X × Y, and ∀ i, X i: basic instances for R1Space;
• IsCompact.mem_closure_iff_exists_inseparable, IsCompact.closure_eq_biUnion_inseparable: characterizations of the closure of a compact set in a preregular space;
• Inseparable.mem_measurableSet_iff: topologically inseparable points can't be separated by a Borel measurable set;
• IsCompact.closure_subset_measurableSet, IsCompact.measure_closure: in a preregular space, a measurable superset of a compact set includes its closure as well; as a corollary, closure K has the same measure as K.
• exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds: an auxiliary lemma extracted from a LocallyCompactPair instance;
• IsCompact.isCompact_isClosed_basis_nhds: if x admits a compact neighborhood, then it admits a basis of compact closed neighborhoods; in particular, a weakly locally compact preregular space is a locally compact regular space;
• isCompact_isClosed_basis_nhds: a version of the previous theorem for weakly locally compact spaces;
• exists_mem_nhds_isCompact_isClosed: in a locally compact regular space, each point admits a compact closed neighborhood.

Deprecated theorems

Some theorems about topological groups are true for any (pre)regular space, so we deprecate the special cases.

• exists_isCompact_isClosed_subset_isCompact_nhds_one: use new IsCompact.isCompact_isClosed_basis_nhds instead;
• instLocallyCompactSpaceOfWeaklyOfGroup, instLocallyCompactSpaceOfWeaklyOfAddGroup: are now implied by WeaklyLocallyCompactSpace.locallyCompactSpace;
• local_isCompact_isClosed_nhds_of_group, local_isCompact_isClosed_nhds_of_addGroup: use isCompact_isClosed_basis_nhds instead;
• exists_isCompact_isClosed_nhds_one, exists_isCompact_isClosed_nhds_zero: use exists_mem_nhds_isCompact_isClosed instead.

Renamed/moved theorems

For each renamed theorem, the old theorem is redefined as a deprecated alias.

• isOpen_setOf_disjoint_nhds_nhds: moved to Constructions;
• isCompact_closure_of_subset_compact -> IsCompact.closure_of_subset;
• IsCompact.measure_eq_infi_isOpen -> IsCompact.measure_eq_iInf_isOpen;
• exists_compact_superset_iff -> exists_isCompact_superset_iff;
• separatedNhds_of_isCompact_isCompact_isClosed -> SeparatedNhds.of_isCompact_isCompact_isClosed;
• separatedNhds_of_isCompact_isCompact -> SeparatedNhds.of_isCompact_isCompact;
• separatedNhds_of_finset_finset -> SeparatedNhds.of_finset_finset;
• point_disjoint_finset_opens_of_t2 -> SeparatedNhds.of_singleton_finset;
• separatedNhds_of_isCompact_isClosed -> SeparatedNhds.of_isCompact_isClosed;
• exists_open_superset_and_isCompact_closure -> exists_isOpen_superset_and_isCompact_closure;
• exists_open_with_compact_closure -> exists_isOpen_mem_isCompact_closure;