From bf815bd5bd5a500e92450380a3d22db6fe5bfbeb Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 12 Sep 2023 17:41:29 +0000 Subject: [PATCH] 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 --- .../Complex/UpperHalfPlane/Topology.lean | 6 +- Mathlib/Geometry/Manifold/Metrizable.lean | 1 - .../Geometry/Manifold/PartitionOfUnity.lean | 2 - .../Function/ContinuousMapDense.lean | 2 +- Mathlib/Topology/Category/CompHaus/Basic.lean | 2 - .../Topology/Compactification/OnePoint.lean | 8 +- .../Topology/ContinuousFunction/Ideals.lean | 2 - .../Topology/EMetricSpace/Paracompact.lean | 11 +- Mathlib/Topology/Homeomorph.lean | 5 +- Mathlib/Topology/Instances/AddCircle.lean | 5 +- Mathlib/Topology/Instances/ENNReal.lean | 2 +- Mathlib/Topology/MetricSpace/Metrizable.lean | 1 - Mathlib/Topology/Paracompact.lean | 17 +-- Mathlib/Topology/Separation.lean | 128 ++++++++++-------- Mathlib/Topology/StoneCech.lean | 1 - Mathlib/Topology/SubsetProperties.lean | 12 +- Mathlib/Topology/UniformSpace/Compact.lean | 3 +- 17 files changed, 105 insertions(+), 103 deletions(-) diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean index 400713858e806..d8dc9393f1aac 100644 --- a/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean +++ b/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean @@ -54,11 +54,9 @@ theorem continuous_im : Continuous im := instance : TopologicalSpace.SecondCountableTopology ℍ := TopologicalSpace.Subtype.secondCountableTopology _ -instance : T3Space ℍ := - Subtype.t3Space +instance : T3Space ℍ := Subtype.t3Space -instance : NormalSpace ℍ := - normalSpaceOfT3SecondCountable ℍ +instance : T4Space ℍ := inferInstance instance : ContractibleSpace ℍ := (convex_halfspace_im_gt 0).contractibleSpace ⟨I, one_pos.trans_eq I_im.symm⟩ diff --git a/Mathlib/Geometry/Manifold/Metrizable.lean b/Mathlib/Geometry/Manifold/Metrizable.lean index 2afd8a37cdb42..6d37d40b92913 100644 --- a/Mathlib/Geometry/Manifold/Metrizable.lean +++ b/Mathlib/Geometry/Manifold/Metrizable.lean @@ -26,7 +26,6 @@ theorem ManifoldWithCorners.metrizableSpace {E : Type*} [NormedAddCommGroup E] [ (M : Type*) [TopologicalSpace M] [ChartedSpace H M] [SigmaCompactSpace M] [T2Space M] : MetrizableSpace M := by haveI := I.locallyCompactSpace; haveI := ChartedSpace.locallyCompactSpace H M - haveI : NormalSpace M := normal_of_paracompact_t2 haveI := I.secondCountableTopology haveI := ChartedSpace.secondCountable_of_sigma_compact H M exact metrizableSpace_of_t3_second_countable M diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 8df63583ae44b..7d55c8b1d8b63 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -343,7 +343,6 @@ theorem exists_isSubordinate [T2Space M] [SigmaCompactSpace M] (hs : IsClosed s) -- First we deduce some missing instances haveI : LocallyCompactSpace H := I.locallyCompactSpace haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M - haveI : NormalSpace M := normal_of_paracompact_t2 -- Next we choose a covering by supports of smooth bump functions have hB := fun x hx => SmoothBumpFunction.nhds_basis_support I (hU x hx) rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs hB with @@ -523,7 +522,6 @@ theorem exists_isSubordinate {s : Set M} (hs : IsClosed s) (U : ι → Set M) (h (hU : s ⊆ ⋃ i, U i) : ∃ f : SmoothPartitionOfUnity ι I M s, f.IsSubordinate U := by haveI : LocallyCompactSpace H := I.locallyCompactSpace haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M - haveI : NormalSpace M := normal_of_paracompact_t2 -- porting note(https://github.com/leanprover/std4/issues/116): -- split `rcases` into `have` + `rcases` have := BumpCovering.exists_isSubordinate_of_prop (Smooth I 𝓘(ℝ)) ?_ hs U ho hU diff --git a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean index 85217d2f4b3c7..cb092300fe588 100644 --- a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean +++ b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean @@ -63,7 +63,7 @@ open scoped ENNReal NNReal Topology BoundedContinuousFunction open MeasureTheory TopologicalSpace ContinuousMap Set -variable {α : Type*} [MeasurableSpace α] [TopologicalSpace α] [NormalSpace α] [BorelSpace α] +variable {α : Type*} [MeasurableSpace α] [TopologicalSpace α] [T4Space α] [BorelSpace α] variable {E : Type*} [NormedAddCommGroup E] {μ : Measure α} {p : ℝ≥0∞} diff --git a/Mathlib/Topology/Category/CompHaus/Basic.lean b/Mathlib/Topology/Category/CompHaus/Basic.lean index 1fd3d3aeaa1a1..ed79094e4ba0b 100644 --- a/Mathlib/Topology/Category/CompHaus/Basic.lean +++ b/Mathlib/Topology/Category/CompHaus/Basic.lean @@ -340,8 +340,6 @@ theorem epi_iff_surjective {X Y : CompHaus.{u}} (f : X ⟶ Y) : Epi f ↔ Functi rw [Set.disjoint_singleton_right] rintro ⟨y', hy'⟩ exact hy y' hy' - --haveI : NormalSpace Y.toTop := normalOfCompactT2 - haveI : NormalSpace ((forget CompHaus).obj Y) := normalOfCompactT2 obtain ⟨φ, hφ0, hφ1, hφ01⟩ := exists_continuous_zero_one_of_closed hC hD hCD haveI : CompactSpace (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.compactSpace haveI : T2Space (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.t2Space diff --git a/Mathlib/Topology/Compactification/OnePoint.lean b/Mathlib/Topology/Compactification/OnePoint.lean index 8df517c25fb97..56cf658f4542d 100644 --- a/Mathlib/Topology/Compactification/OnePoint.lean +++ b/Mathlib/Topology/Compactification/OnePoint.lean @@ -457,14 +457,14 @@ instance [T1Space X] : T1Space (OnePoint X) where · rw [← image_singleton, isClosed_image_coe] exact ⟨isClosed_singleton, isCompact_singleton⟩ -/-- The one point compactification of a locally compact Hausdorff space is a normal (hence, -Hausdorff and regular) topological space. -/ -instance [LocallyCompactSpace X] [T2Space X] : NormalSpace (OnePoint X) := by +/-- The one point compactification of a weakly locally compact Hausdorff space is a T₄ +(hence, Hausdorff and regular) topological space. -/ +instance [WeaklyLocallyCompactSpace X] [T2Space X] : T4Space (OnePoint X) := by have key : ∀ z : X, Disjoint (𝓝 (some z)) (𝓝 ∞) := fun z => by rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact, disjoint_map coe_injective, ← principal_singleton, disjoint_principal_right, compl_infty] exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩ - suffices : T2Space (OnePoint X); exact normalOfCompactT2 + suffices : T2Space (OnePoint X); infer_instance refine t2Space_iff_disjoint_nhds.2 fun x y hxy => ?_ induction x using OnePoint.rec <;> induction y using OnePoint.rec · exact (hxy rfl).elim diff --git a/Mathlib/Topology/ContinuousFunction/Ideals.lean b/Mathlib/Topology/ContinuousFunction/Ideals.lean index 46f7fd440c87c..2d39b99956ba1 100644 --- a/Mathlib/Topology/ContinuousFunction/Ideals.lean +++ b/Mathlib/Topology/ContinuousFunction/Ideals.lean @@ -321,7 +321,6 @@ theorem setOfIdeal_ofSet_eq_interior (s : Set X) : setOfIdeal (idealOfSet 𝕜 s -- If `x ∉ closure sᶜ`, we must produce `f : C(X, 𝕜)` which is zero on `sᶜ` and `f x ≠ 0`. rw [← compl_compl (interior s), ← closure_compl] at hx simp_rw [mem_setOfIdeal, mem_idealOfSet] - haveI : NormalSpace X := normalOfCompactT2 /- Apply Urysohn's lemma to get `g : C(X, ℝ)` which is zero on `sᶜ` and `g x ≠ 0`, then compose with the natural embedding `ℝ ↪ 𝕜` to produce the desired `f`. -/ obtain ⟨g, hgs, hgx : Set.EqOn g 1 {x}, -⟩ := @@ -436,7 +435,6 @@ variable [CompactSpace X] [T2Space X] [IsROrC 𝕜] theorem continuousMapEval_bijective : Bijective (continuousMapEval X 𝕜) := by refine' ⟨fun x y hxy => _, fun φ => _⟩ · contrapose! hxy - haveI := @normalOfCompactT2 X _ _ _ rcases exists_continuous_zero_one_of_closed (isClosed_singleton : _root_.IsClosed {x}) (isClosed_singleton : _root_.IsClosed {y}) (Set.disjoint_singleton.mpr hxy) with ⟨f, fx, fy, -⟩ diff --git a/Mathlib/Topology/EMetricSpace/Paracompact.lean b/Mathlib/Topology/EMetricSpace/Paracompact.lean index 536e7a5168952..d19cb5f8c9190 100644 --- a/Mathlib/Topology/EMetricSpace/Paracompact.lean +++ b/Mathlib/Topology/EMetricSpace/Paracompact.lean @@ -35,8 +35,8 @@ open ENNReal Topology Set namespace EMetric -- See note [lower instance priority] -/-- A `PseudoEMetricSpace` is always a paracompact space. Formalization is based -on [MR0236876]. -/ +/-- A `PseudoEMetricSpace` is always a paracompact space. +Formalization is based on [MR0236876]. -/ instance (priority := 100) instParacompactSpace [PseudoEMetricSpace α] : ParacompactSpace α := by /- We start with trivial observations about `1 / 2 ^ k`. Here and below we use `1 / 2 ^ k` in the comments and `2⁻¹ ^ k` in the code. -/ @@ -166,9 +166,8 @@ instance (priority := 100) instParacompactSpace [PseudoEMetricSpace α] : Paraco exact not_lt.1 fun hlt => (Hgt I.1 hlt I.2).le_bot hI.choose_spec #align emetric.paracompact_space EMetric.instParacompactSpace --- see Note [lower instance priority] -instance (priority := 100) instNormalSpace [EMetricSpace α] : NormalSpace α := - normal_of_paracompact_t2 -#align emetric.normal_of_emetric EMetric.instNormalSpace +-- porting note: no longer an instance because `inferInstance` can find it +theorem t4Space [EMetricSpace α] : T4Space α := inferInstance +#align emetric.normal_of_emetric EMetric.t4Space end EMetric diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean index 0cfb21edd9a3c..4e598538d894e 100644 --- a/Mathlib/Topology/Homeomorph.lean +++ b/Mathlib/Topology/Homeomorph.lean @@ -360,7 +360,10 @@ protected theorem closedEmbedding (h : α ≃ₜ β) : ClosedEmbedding h := protected theorem normalSpace [NormalSpace α] (h : α ≃ₜ β) : NormalSpace β := h.symm.closedEmbedding.normalSpace -#align homeomorph.normal_space Homeomorph.normalSpace + +protected theorem t4Space [T4Space α] (h : α ≃ₜ β) : T4Space β := + h.symm.closedEmbedding.t4Space +#align homeomorph.normal_space Homeomorph.t4Space theorem preimage_closure (h : α ≃ₜ β) (s : Set β) : h ⁻¹' closure s = closure (h ⁻¹' s) := h.isOpenMap.preimage_closure_eq_closure_preimage h.continuous _ diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index d10558eef48b0..740116b146fd1 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -525,9 +525,8 @@ instance : ProperlyDiscontinuousVAdd (AddSubgroup.opposite (zmultiples p)) ℝ : instance : T2Space (AddCircle p) := t2Space_of_properlyDiscontinuousVAdd_of_t2Space -/-- The "additive circle" `ℝ ⧸ (ℤ ∙ p)` is normal. -/ -instance [Fact (0 < p)] : NormalSpace (AddCircle p) := - normalOfCompactT2 +/-- The "additive circle" `ℝ ⧸ (ℤ ∙ p)` is T₄. -/ +instance [Fact (0 < p)] : T4Space (AddCircle p) := inferInstance /-- The "additive circle" `ℝ ⧸ (ℤ ∙ p)` is second-countable. -/ instance : SecondCountableTopology (AddCircle p) := diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean index 7cac804e3bb52..8c521fef83338 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal.lean @@ -42,7 +42,7 @@ instance : OrderTopology ℝ≥0∞ := ⟨rfl⟩ -- short-circuit type class inference instance : T2Space ℝ≥0∞ := inferInstance instance : T5Space ℝ≥0∞ := inferInstance -instance : NormalSpace ℝ≥0∞ := inferInstance +instance : T4Space ℝ≥0∞ := inferInstance instance : SecondCountableTopology ℝ≥0∞ := orderIsoUnitIntervalBirational.toHomeomorph.embedding.secondCountableTopology diff --git a/Mathlib/Topology/MetricSpace/Metrizable.lean b/Mathlib/Topology/MetricSpace/Metrizable.lean index 56bfc5bd431e1..591f5728f3811 100644 --- a/Mathlib/Topology/MetricSpace/Metrizable.lean +++ b/Mathlib/Topology/MetricSpace/Metrizable.lean @@ -150,7 +150,6 @@ variable [T3Space X] [SecondCountableTopology X] /-- A T₃ topological space with second countable topology can be embedded into `l^∞ = ℕ →ᵇ ℝ`. -/ theorem exists_embedding_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Embedding f := by - haveI : NormalSpace X := normalSpaceOfT3SecondCountable X -- Choose a countable basis, and consider the set `s` of pairs of set `(U, V)` such that `U ∈ B`, -- `V ∈ B`, and `closure U ⊆ V`. rcases exists_countable_basis X with ⟨B, hBc, -, hB⟩ diff --git a/Mathlib/Topology/Paracompact.lean b/Mathlib/Topology/Paracompact.lean index 5f240bcdc8995..59cf17640218b 100644 --- a/Mathlib/Topology/Paracompact.lean +++ b/Mathlib/Topology/Paracompact.lean @@ -287,17 +287,18 @@ instance (priority := 100) paracompact_of_locallyCompact_sigmaCompact [WeaklyLoc exact ⟨β, t, fun x ↦ (hto x).1.2, htc, htf, fun b ↦ ⟨i <| c b, (hto b).2⟩⟩ #align paracompact_of_locally_compact_sigma_compact paracompact_of_locallyCompact_sigmaCompact -/- Dieudonné's theorem: a paracompact Hausdorff space is normal. Formalization is based on the proof +/- **Dieudonné's theorem**: a paracompact Hausdorff space is normal. +Formalization is based on the proof at [ncatlab](https://ncatlab.org/nlab/show/paracompact+Hausdorff+spaces+are+normal). -/ -theorem normal_of_paracompact_t2 [T2Space X] [ParacompactSpace X] : NormalSpace X := by +instance (priority := 100) T4Space.of_paracompactSpace_t2Space [T2Space X] [ParacompactSpace X] : + T4Space X := by -- First we show how to go from points to a set on one side. - have : ∀ s t : Set X, IsClosed s → IsClosed t → + have : ∀ s t : Set X, IsClosed s → (∀ x ∈ s, ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) → - ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v := by + ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v := fun s t hs H ↦ by /- For each `x ∈ s` we choose open disjoint `u x ∋ x` and `v x ⊇ t`. The sets `u x` form an open covering of `s`. We choose a locally finite refinement `u' : s → Set X`, then `⋃ i, u' i` and `(closure (⋃ i, u' i))ᶜ` are disjoint open neighborhoods of `s` and `t`. -/ - intro s t hs _ H choose u v hu hv hxu htv huv using SetCoe.forall'.1 H rcases precise_refinement_set hs u hu fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, hxu _⟩ with ⟨u', hu'o, hcov', hu'fin, hsub⟩ @@ -308,10 +309,10 @@ theorem normal_of_paracompact_t2 [T2Space X] [ParacompactSpace X] : NormalSpace absurd (htv i hxt) (closure_minimal _ (isClosed_compl_iff.2 <| hv _) hxu) exact fun y hyu hyv ↦ (huv i).le_bot ⟨hsub _ hyu, hyv⟩ -- Now we apply the lemma twice: first to `s` and `t`, then to `t` and each point of `s`. - refine' ⟨fun s t hs ht hst ↦ this s t hs ht fun x hx ↦ _⟩ - rcases this t {x} ht isClosed_singleton fun y hy ↦ (by + refine { normal := fun s t hs ht hst ↦ this s t hs fun x hx ↦ ?_ } + rcases this t {x} ht fun y hy ↦ (by simp_rw [singleton_subset_iff] exact t2_separation (hst.symm.ne_of_mem hy hx)) with ⟨v, u, hv, hu, htv, hxu, huv⟩ exact ⟨u, v, hu, hv, singleton_subset_iff.1 hxu, htv, huv.symm⟩ -#align normal_of_paracompact_t2 normal_of_paracompact_t2 +#align normal_of_paracompact_t2 T4Space.of_paracompactSpace_t2Space diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index b4367e8797dbc..0d5256cc2801b 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -31,9 +31,9 @@ This file defines the predicate `SeparatedNhds`, and common separation axioms there is two open sets, one containing `x`, and the other `y`, whose closures are disjoint. * `T3Space`: A T₃ space, is one where given any closed `C` and `x ∉ C`, there is disjoint open sets containing `x` and `C` respectively. In `mathlib`, T₃ implies T₂.₅. -* `NormalSpace`: A T₄ space (sometimes referred to as normal, but authors vary on - whether this includes T₂; `mathlib` does), is one where given two disjoint closed sets, - we can find two open sets that separate them. In `mathlib`, T₄ implies T₃. +* `NormalSpace`: A normal space, is one where given two disjoint closed sets, + we can find two open sets that separate them. +* `T4Space`: A T₄ space is a normal T₁ space. T₄ implies T₃. * `T5Space`: A T₅ space, also known as a *completely normal Hausdorff space* ## Main results @@ -1735,22 +1735,23 @@ instance [RegularSpace α] : T3Space (SeparationQuotient α) where end T3 -section Normality +section NormalSpace --- todo: rename this to `T4Space`, introduce `NormalSpace` without `T1Space` assumption -/-- A T₄ space, also known as a normal space (although this condition sometimes - omits T₂), is one in which for every pair of disjoint closed sets `C` and `D`, - there exist disjoint open sets containing `C` and `D` respectively. -/ -class NormalSpace (α : Type u) [TopologicalSpace α] extends T1Space α : Prop where +/-- A topological space is said to be a *normal space* if any two disjoint closed sets +have disjoint open neighborhoods. -/ +class NormalSpace (X : Type u) [TopologicalSpace X] : Prop where /-- Two disjoint sets in a normal space admit disjoint neighbourhoods. -/ - normal : ∀ s t : Set α, IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t -#align normal_space NormalSpace + normal : ∀ s t : Set X, IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t theorem normal_separation [NormalSpace α] {s t : Set α} (H1 : IsClosed s) (H2 : IsClosed t) (H3 : Disjoint s t) : SeparatedNhds s t := NormalSpace.normal s t H1 H2 H3 #align normal_separation normal_separation +theorem disjoint_nhdsSet_nhdsSet [NormalSpace α] {s t : Set α} (hs : IsClosed s) (ht : IsClosed t) + (hd : Disjoint s t) : Disjoint (𝓝ˢ s) (𝓝ˢ t) := + (normal_separation hs ht hd).disjoint_nhdsSet + theorem normal_exists_closure_subset [NormalSpace α] {s t : Set α} (hs : IsClosed s) (ht : IsOpen t) (hst : s ⊆ t) : ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t := by have : Disjoint s tᶜ := Set.disjoint_left.mpr fun x hxs hxt => hxt (hst hxs) @@ -1761,49 +1762,18 @@ theorem normal_exists_closure_subset [NormalSpace α] {s t : Set α} (hs : IsClo exact fun x hxs hxt => hs't'.le_bot ⟨hxs, hxt⟩ #align normal_exists_closure_subset normal_exists_closure_subset --- see Note [lower instance priority] -instance (priority := 100) NormalSpace.t3Space [NormalSpace α] : T3Space α where - regular hs hxs := by simpa only [nhdsSet_singleton] using (normal_separation hs isClosed_singleton - (disjoint_singleton_right.mpr hxs)).disjoint_nhdsSet -#align normal_space.t3_space NormalSpace.t3Space - --- We can't make this an instance because it could cause an instance loop. --- porting note: todo: now we can -theorem normalOfCompactT2 [CompactSpace α] [T2Space α] : NormalSpace α := - ⟨fun _s _t hs ht => isCompact_isCompact_separated hs.isCompact ht.isCompact⟩ -#align normal_of_compact_t2 normalOfCompactT2 - +/-- If the codomain of a closed embedding is a normal space, then so is the domain. -/ protected theorem ClosedEmbedding.normalSpace [TopologicalSpace β] [NormalSpace β] {f : α → β} (hf : ClosedEmbedding f) : NormalSpace α where - toT1Space := hf.toEmbedding.t1Space normal s t hs ht hst := by have H : SeparatedNhds (f '' s) (f '' t) := NormalSpace.normal (f '' s) (f '' t) (hf.isClosedMap s hs) (hf.isClosedMap t ht) (disjoint_image_of_injective hf.inj hst) exact (H.preimage hf.continuous).mono (subset_preimage_image _ _) (subset_preimage_image _ _) -#align closed_embedding.normal_space ClosedEmbedding.normalSpace - -namespace SeparationQuotient -/-- The `SeparationQuotient` of a normal space is a T₄ space. We don't have separate typeclasses -for normal spaces (without T₁ assumption) and T₄ spaces, so we use the same class for assumption -and for conclusion. - -One can prove this using a homeomorphism between `α` and `SeparationQuotient α`. We give an -alternative proof that works without assuming that `α` is a T₁ space. -/ -instance [NormalSpace α] : NormalSpace (SeparationQuotient α) where - normal s t hs ht hd := separatedNhds_iff_disjoint.2 <| by - rw [← disjoint_comap_iff surjective_mk, comap_mk_nhdsSet, comap_mk_nhdsSet] - exact (normal_separation (hs.preimage continuous_mk) (ht.preimage continuous_mk) - (hd.preimage mk)).disjoint_nhdsSet - -end SeparationQuotient - -variable (α) - -/-- A T₃ topological space with second countable topology is a normal space. -This lemma is not an instance to avoid a loop. -/ -theorem normalSpaceOfT3SecondCountable [SecondCountableTopology α] [T3Space α] : NormalSpace α := by +/-- A regular topological space with second countable topology is a normal space. -/ +instance (priority := 100) NormalSpace.of_regularSpace_secondCountableTopology + [RegularSpace α] [SecondCountableTopology α] : NormalSpace α := by have key : ∀ {s t : Set α}, IsClosed t → Disjoint s t → ∃ U : Set (countableBasis α), (s ⊆ ⋃ u ∈ U, ↑u) ∧ (∀ u ∈ U, Disjoint (closure ↑u) t) ∧ ∀ n : ℕ, IsClosed (⋃ (u ∈ U) (_ : Encodable.encode u ≤ n), closure (u : Set α)) := by @@ -1822,7 +1792,7 @@ theorem normalSpaceOfT3SecondCountable [SecondCountableTopology α] [T3Space α] · simp only [← iSup_eq_iUnion, iSup_and'] exact (((finite_le_nat n).preimage_embedding (Encodable.encode' _)).subset <| inter_subset_right _ _).isClosed_biUnion fun u _ => isClosed_closure - refine' ⟨fun s t hs ht hd => _⟩ + refine' { normal := fun s t hs ht hd => _ } rcases key ht hd with ⟨U, hsU, hUd, hUc⟩ rcases key hs hd.symm with ⟨V, htV, hVd, hVc⟩ refine ⟨⋃ u ∈ U, ↑u \ ⋃ (v ∈ V) (_ : Encodable.encode v ≤ Encodable.encode u), closure ↑v, @@ -1844,7 +1814,48 @@ theorem normalSpaceOfT3SecondCountable [SecondCountableTopology α] [T3Space α] rintro a ⟨u, huU, hau, haV⟩ v hvV hav cases' le_total (Encodable.encode u) (Encodable.encode v) with hle hle exacts [⟨u, huU, hle, subset_closure hau⟩, (haV _ hvV hle <| subset_closure hav).elim] -#align normal_space_of_t3_second_countable normalSpaceOfT3SecondCountable +#align normal_space_of_t3_second_countable NormalSpace.of_regularSpace_secondCountableTopology + +end NormalSpace + +section Normality + +/-- A T₄ space is a normal T₁ space. -/ +class T4Space (α : Type u) [TopologicalSpace α] extends T1Space α, NormalSpace α : Prop +#align normal_space NormalSpace + +instance (priority := 100) [T1Space α] [NormalSpace α] : T4Space α := ⟨⟩ + +-- see Note [lower instance priority] +instance (priority := 100) T4Space.t3Space [T4Space α] : T3Space α where + regular hs hxs := by simpa only [nhdsSet_singleton] using (normal_separation hs isClosed_singleton + (disjoint_singleton_right.mpr hxs)).disjoint_nhdsSet +#align normal_space.t3_space T4Space.t3Space + +instance (priority := 100) T4Space.of_compactSpace_t2Space [CompactSpace α] [T2Space α] : + T4Space α where + normal _s _t hs ht := isCompact_isCompact_separated hs.isCompact ht.isCompact +#align normal_of_compact_t2 T4Space.of_compactSpace_t2Space + +/-- If the codomain of a closed embedding is a T₄ space, then so is the domain. -/ +protected theorem ClosedEmbedding.t4Space [TopologicalSpace β] [T4Space β] {f : α → β} + (hf : ClosedEmbedding f) : T4Space α where + toT1Space := hf.toEmbedding.t1Space + toNormalSpace := hf.normalSpace +#align closed_embedding.normal_space ClosedEmbedding.t4Space + +namespace SeparationQuotient + +/-- The `SeparationQuotient` of a normal space is a normal space. -/ +instance [NormalSpace α] : NormalSpace (SeparationQuotient α) where + normal s t hs ht hd := separatedNhds_iff_disjoint.2 <| by + rw [← disjoint_comap_iff surjective_mk, comap_mk_nhdsSet, comap_mk_nhdsSet] + exact disjoint_nhdsSet_nhdsSet (hs.preimage continuous_mk) (ht.preimage continuous_mk) + (hd.preimage mk) + +end SeparationQuotient + +variable (α) end Normality @@ -1881,19 +1892,20 @@ instance [T5Space α] {p : α → Prop} : T5Space { x // p x } := -- see Note [lower instance priority] /-- A `T₅` space is a `T₄` space. -/ -instance (priority := 100) T5Space.toNormalSpace [T5Space α] : NormalSpace α := - ⟨fun s t hs ht hd => separatedNhds_iff_disjoint.2 <| - completely_normal (by rwa [hs.closure_eq]) (by rwa [ht.closure_eq])⟩ -#align t5_space.to_normal_space T5Space.toNormalSpace +instance (priority := 100) T5Space.toT4Space [T5Space α] : T4Space α where + normal s t hs ht hd := separatedNhds_iff_disjoint.2 <| + completely_normal (by rwa [hs.closure_eq]) (by rwa [ht.closure_eq]) +#align t5_space.to_normal_space T5Space.toT4Space open SeparationQuotient -/-- The `SeparationQuotient` of a completely normal space is a T₅ space. We don't have separate -typeclasses for completely normal spaces (without T₁ assumption) and T₅ spaces, so we use the same -class for assumption and for conclusion. +/-- The `SeparationQuotient` of a completely normal R₀ space is a T₅ space. +We don't have typeclasses for completely normal spaces (without T₁ assumption) and R₀ spaces, +so we use `T5Space` for assumption and for conclusion. -One can prove this using a homeomorphism between `α` and `SeparationQuotient α`. We give an -alternative proof that works without assuming that `α` is a T₁ space. -/ +One can prove this using a homeomorphism between `α` and `SeparationQuotient α`. +We give an alternative proof of the `completely_normal` axiom +that works without assuming that `α` is a T₁ space. -/ instance [T5Space α] : T5Space (SeparationQuotient α) where completely_normal s t hd₁ hd₂ := by rw [← disjoint_comap_iff surjective_mk, comap_mk_nhdsSet, comap_mk_nhdsSet] @@ -1916,13 +1928,11 @@ theorem connectedComponent_eq_iInter_clopen [T2Space α] [CompactSpace α] (x : isClosed_iInter fun Z => Z.2.1.2 rw [isPreconnected_iff_subset_of_fully_disjoint_closed hs] intro a b ha hb hab ab_disj - haveI := @normalOfCompactT2 α _ _ _ -- Since our space is normal, we get two larger disjoint open sets containing the disjoint -- closed sets. If we can show that our intersection is a subset of any of these we can then -- "descend" this to show that it is a subset of either a or b. rcases normal_separation ha hb ab_disj with ⟨u, v, hu, hv, hau, hbv, huv⟩ obtain ⟨Z, H⟩ : ∃ Z : Set α, IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v - /- Now we find a clopen set `Z` around `x`, contained in `u ∪ v`. We utilize the fact that `X \ u ∪ v` will be compact, so there must be some finite intersection of clopen neighbourhoods of `X` disjoint to it, but a finite intersection of clopen sets is clopen so we let this be our diff --git a/Mathlib/Topology/StoneCech.lean b/Mathlib/Topology/StoneCech.lean index 2cfeeb535a579..9392c6eed2f5b 100644 --- a/Mathlib/Topology/StoneCech.lean +++ b/Mathlib/Topology/StoneCech.lean @@ -191,7 +191,6 @@ theorem continuous_ultrafilter_extend (f : α → γ) : Continuous (Ultrafilter. isCompact_univ.ultrafilter_le_nhds (b.map f) (by rw [le_principal_iff]; exact univ_mem) ⟨c, le_trans (map_mono (ultrafilter_comap_pure_nhds _)) h'⟩ letI : TopologicalSpace α := ⊥ - haveI : NormalSpace γ := normalOfCompactT2 exact denseInducing_pure.continuous_extend h #align continuous_ultrafilter_extend continuous_ultrafilter_extend diff --git a/Mathlib/Topology/SubsetProperties.lean b/Mathlib/Topology/SubsetProperties.lean index 6cfd0d1810030..e5af8d33725b8 100644 --- a/Mathlib/Topology/SubsetProperties.lean +++ b/Mathlib/Topology/SubsetProperties.lean @@ -1104,6 +1104,13 @@ theorem exists_compact_superset [WeaklyLocallyCompactSpace α] {K : Set α} (hK exact iUnion₂_subset fun x hx ↦ interior_mono <| subset_iUnion₂ (s := fun x _ ↦ s x) x hx #align exists_compact_superset exists_compact_superset +/-- In a weakly locally compact space, +the filters `𝓝 x` and `cocompact α` are disjoint for all `α`. -/ +theorem disjoint_nhds_cocompact [WeaklyLocallyCompactSpace α] (x : α) : + Disjoint (𝓝 x) (cocompact α) := + let ⟨_, hc, hx⟩ := exists_compact_mem_nhds x + disjoint_of_disjoint_of_mem disjoint_compl_right hx hc.compl_mem_cocompact + /-- There are various definitions of "locally compact space" in the literature, which agree for Hausdorff spaces but not in general. This one is the precise condition on X needed @@ -1128,11 +1135,6 @@ theorem local_compact_nhds [LocallyCompactSpace α] {x : α} {n : Set α} (h : n LocallyCompactSpace.local_compact_nhds _ _ h #align local_compact_nhds local_compact_nhds -/-- In a locally compact space, the filters `𝓝 x` and `cocompact α` are disjoint for all `α`. -/ -theorem disjoint_nhds_cocompact [LocallyCompactSpace α] (x : α) : Disjoint (𝓝 x) (cocompact α) := - let ⟨_, hx, _, hc⟩ := local_compact_nhds (univ_mem (f := 𝓝 x)); - disjoint_of_disjoint_of_mem disjoint_compl_right hx hc.compl_mem_cocompact - theorem locallyCompactSpace_of_hasBasis {ι : α → Type*} {p : ∀ x, ι x → Prop} {s : ∀ x, ι x → Set α} (h : ∀ x, (𝓝 x).HasBasis (p x) (s x)) (hc : ∀ x i, p x i → IsCompact (s x i)) : LocallyCompactSpace α := diff --git a/Mathlib/Topology/UniformSpace/Compact.lean b/Mathlib/Topology/UniformSpace/Compact.lean index c2b52c64a7f94..78a829727c238 100644 --- a/Mathlib/Topology/UniformSpace/Compact.lean +++ b/Mathlib/Topology/UniformSpace/Compact.lean @@ -103,8 +103,7 @@ def uniformSpaceOfCompactT2 [TopologicalSpace γ] [CompactSpace γ] [T2Space γ] rwa [closure_compl] at this have diag_subset : diagonal γ ⊆ interior V := subset_interior_iff_mem_nhdsSet.2 V_in have x_ne_y : x ≠ y := mt (@diag_subset (x, y)) this - -- Since γ is compact and Hausdorff, it is normal, hence T₃. - haveI : NormalSpace γ := normalOfCompactT2 + -- Since γ is compact and Hausdorff, it is T₄, hence T₃. -- So there are closed neighborhoods V₁ and V₂ of x and y contained in -- disjoint open neighborhoods U₁ and U₂. obtain