Commit 2023-09-12 17:41 bf815bd5

View on Github →

refactor: split NormalSpace into NormalSpace and T4Space (#7072)

Rename NormalSpace to T4Space.
Add NormalSpace, a version without the T1Space assumption.
Adjust some theorems.
Supersedes thus closes #6892.
Add some instance cycles, see #2030

Estimated changes

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

Modified Mathlib/Geometry/Manifold/Metrizable.lean

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

Modified Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

Modified Mathlib/Topology/Category/CompHaus/Basic.lean

Modified Mathlib/Topology/Compactification/OnePoint.lean

Modified Mathlib/Topology/ContinuousFunction/Ideals.lean

Modified Mathlib/Topology/EMetricSpace/Paracompact.lean

added theorem EMetric.t4Space

Modified Mathlib/Topology/Homeomorph.lean

Modified Mathlib/Topology/Instances/AddCircle.lean

Modified Mathlib/Topology/Instances/ENNReal.lean

Modified Mathlib/Topology/MetricSpace/Metrizable.lean

Modified Mathlib/Topology/Paracompact.lean

deleted theorem normal_of_paracompact_t2

Modified Mathlib/Topology/Separation.lean

added theorem disjoint_nhdsSet_nhdsSet

deleted theorem normalOfCompactT2

deleted theorem normalSpaceOfT3SecondCountable

Modified Mathlib/Topology/StoneCech.lean

Modified Mathlib/Topology/SubsetProperties.lean

modified theorem disjoint_nhds_cocompact

Modified Mathlib/Topology/UniformSpace/Compact.lean