Commit 2024-03-01 09:34 ad081918

View on Github →

chore(Separation): rename some lemmas (#11054) Mathport chose wrong names for these constructors.

Estimated changes

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Separation.lean

deleted theorem RegularSpace.ofBasis

deleted theorem RegularSpace.ofExistsMemNhdsIsClosedSubset

deleted theorem RegularSpace.ofLift'_closure

added theorem RegularSpace.of_exists_mem_nhds_isClosed_subset

added theorem RegularSpace.of_hasBasis

added theorem RegularSpace.of_lift'_closure

Modified Mathlib/Topology/UniformSpace/Separation.lean