Commit 2025-05-07 15:35 e3aeb666

View on Github →

feat: Metric Spaces are T6 (#22256) This PR shows that metric spaces are T6. It also generalizes the contents of Mathlib/Topology/GDelta/UniformSpace to apply to metrizable spaces. See this Zulip thread.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/Order/Interval/Set/Disjoint.lean

added theorem Set.Iio_disjoint_Ioi_iff

added theorem Set.Iio_disjoint_Ioi_of_le

added theorem Set.Iio_disjoint_Ioi_of_not_lt

added theorem Set.Iio_disjoint_Ioi_same

added theorem Set.Ioi_disjoint_Iio_iff

added theorem Set.Ioi_disjoint_Iio_of_le

added theorem Set.Ioi_disjoint_Iio_of_not_lt

added theorem Set.Ioi_disjoint_Iio_same

Modified Mathlib/Topology/Baire/BaireMeasurable.lean

Modified Mathlib/Topology/GDelta/Basic.lean

Created Mathlib/Topology/GDelta/MetrizableSpace.lean

added theorem IsGδ.setOf_continuousAt

Deleted Mathlib/Topology/GDelta/UniformSpace.lean

deleted theorem IsClosed.isGδ

deleted theorem IsGδ.setOf_continuousAt

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

Modified Mathlib/Topology/Metrizable/Basic.lean

Modified Mathlib/Topology/Metrizable/Uniformity.lean

Modified Mathlib/Topology/Separation/GDelta.lean

added theorem IsClosed.isGδ