Commit 2024-03-10 19:38 38155ec4

View on Github →

refactor(UniformSpace): drop separationRel (#10644) We had duplicated API between topological spaces and uniform spaces. In this PR I mostly deduplicate it with some exceptions:

  • SeparationQuotient.lift' and SeparationQuotient.map are leftovers from the old version that are designed to work with uniform spaces;
  • probably, some theorems/instances still assume UniformSpace when TopologicalSpace would work. Outside of UniformSpace/Separation, I mostly changed SeparatedSpace to T0Space and separationRel to Inseparable. I also rewrote a few proofs that were broken by the API change. Fixes #2031

Estimated changes

modified theorem IsCompactOperator.restrict'
added theorem group_inseparable_iff
modified theorem AddMonoidHom.extension_coe
deleted theorem group_separationRel
modified theorem UniformSpace.ring_sep_quot
deleted theorem UniformSpace.ring_sep_rel
modified theorem CpltSepUniformSpace.coe_of
modified theorem IsComplete.isClosed
modified theorem eq_of_clusterPt_uniformity
modified theorem eq_of_forall_symmetric
modified theorem eq_of_uniformity
modified theorem eq_of_uniformity_basis
deleted theorem idRel_sub_separationRel
modified theorem isClosed_of_spaced_out
deleted theorem isClosed_separationRel
deleted theorem separatedSpace_iff
deleted theorem separated_def'
deleted theorem separated_def
deleted theorem separated_equiv
deleted theorem separated_iff_t2
deleted def separationRel
deleted theorem separationRel_comap
added theorem t0Space_iff_uniformity