Commit 2024-10-25 08:08 d85e7dbb

View on Github →

chore: split Topology.Separation (#18213) Avoids needing GDelta / UniformSpace in many later files. (Identified using #18156)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convex/Radon.lean

Modified Mathlib/Dynamics/FixedPoints/Topology.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Defs.lean

Modified Mathlib/Topology/Algebra/Semigroup.lean

Modified Mathlib/Topology/Compactification/OnePoint.lean

Modified Mathlib/Topology/Connected/Separation.lean

Modified Mathlib/Topology/CountableSeparatingOn.lean

Modified Mathlib/Topology/DenseEmbedding.lean

Modified Mathlib/Topology/DiscreteQuotient.lean

Modified Mathlib/Topology/DiscreteSubset.lean

Modified Mathlib/Topology/ExtendFrom.lean

Modified Mathlib/Topology/Filter.lean

Modified Mathlib/Topology/IndicatorConstPointwise.lean

Modified Mathlib/Topology/Instances/Irrational.lean

Modified Mathlib/Topology/Order/OrderClosed.lean

Modified Mathlib/Topology/Order/Priestley.lean

Modified Mathlib/Topology/Perfect.lean

Modified Mathlib/Topology/QuasiSeparated.lean

Modified Mathlib/Topology/SeparatedMap.lean

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

deleted theorem Disjoint.hasSeparatingCover_closed_gdelta_right

deleted theorem Finset.isGδ_compl

deleted theorem IsGδ.compl_singleton

deleted theorem Set.Countable.isGδ_compl

deleted theorem Set.Finite.isGδ

deleted theorem Set.Finite.isGδ_compl

deleted theorem Set.Subsingleton.isGδ_compl

Created Mathlib/Topology/Separation/GDelta.lean

added theorem Disjoint.hasSeparatingCover_closed_gdelta_right

added theorem Finset.isGδ_compl

added theorem IsGδ.compl_singleton

added theorem Set.Countable.isGδ_compl

added theorem Set.Finite.isGδ

added theorem Set.Finite.isGδ_compl

added theorem Set.Subsingleton.isGδ_compl

Modified Mathlib/Topology/Separation/NotNormal.lean

Modified Mathlib/Topology/ShrinkingLemma.lean

Modified Mathlib/Topology/Sober.lean

Modified Mathlib/Topology/Specialization.lean

Modified Mathlib/Topology/Support.lean

Modified Mathlib/Topology/UniformSpace/Compact.lean

Modified Mathlib/Topology/UniformSpace/Separation.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergence.lean