Commit 2024-10-25 11:44 086c16c9

View on Github →

chore: split Topology.GDelta (#18215)

Estimated changes

Modified Mathlib.lean

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

Modified Mathlib/Topology/Baire/BaireMeasurable.lean

Modified Mathlib/Topology/Baire/Lemmas.lean

Renamed Mathlib/Topology/GDelta.lean to Mathlib/Topology/GDelta/Basic.lean

deleted theorem IsClosed.isGδ

deleted theorem IsGδ.setOf_continuousAt

Created Mathlib/Topology/GDelta/UniformSpace.lean

added theorem IsClosed.isGδ

added theorem IsGδ.setOf_continuousAt

Modified Mathlib/Topology/Instances/Irrational.lean

Modified Mathlib/Topology/Separation/GDelta.lean

Modified Mathlib/Topology/UrysohnsLemma.lean