feat: +1 proof that Sorgenfrey plane is not normal (#5775)

Author: urkud

Counterexamples/SorgenfreyLine.lean

@@ -14,6 +14,7 @@ import Mathlib.Topology.Paracompact
 import Mathlib.Topology.MetricSpace.Metrizable
 import Mathlib.Topology.MetricSpace.EMetricParacompact
 import Mathlib.Data.Set.Intervals.Monotone
+import Mathlib.Topology.Separation.NotNormal
 
 /-!
 # Sorgenfrey line
@@ -38,7 +39,7 @@ Prove that the Sorgenfrey line is a paracompact space.
 
 open Set Filter TopologicalSpace
 
-open scoped Topology Filter
+open scoped Topology Filter Cardinal
 
 namespace Counterexample
 
@@ -78,7 +79,7 @@ theorem isOpen_Ici (a : ℝₗ) : IsOpen (Ici a) :=
   iUnion_Ico_right a ▸ isOpen_iUnion (isOpen_Ico a)
 #align counterexample.sorgenfrey_line.is_open_Ici Counterexample.SorgenfreyLine.isOpen_Ici
 
-theorem nhds_basis_Ico (a : ℝₗ) : (𝓝 a).HasBasis (fun b => a < b) fun b => Ico a b := by
+theorem nhds_basis_Ico (a : ℝₗ) : (𝓝 a).HasBasis (a < ·) (Ico a ·) := by
   rw [TopologicalSpace.nhds_generateFrom]
   haveI : Nonempty { x // x ≤ a } := Set.nonempty_Iic_subtype
   have : (⨅ x : { i // i ≤ a }, 𝓟 (Ici ↑x)) = 𝓟 (Ici a) := by
@@ -235,9 +236,15 @@ theorem isClopen_Ici_prod (x : ℝₗ × ℝₗ) : IsClopen (Ici x) :=
   (Ici_prod_eq x).symm ▸ (isClopen_Ici _).prod (isClopen_Ici _)
 #align counterexample.sorgenfrey_line.is_clopen_Ici_prod Counterexample.SorgenfreyLine.isClopen_Ici_prod
 
+theorem cardinal_antidiagonal (c : ℝₗ) : #{x : ℝₗ × ℝₗ | x.1 + x.2 = c} = 𝔠 := by
+  rw [← Cardinal.mk_real]
+  exact Equiv.cardinal_eq ⟨fun x ↦ toReal x.1.1,
+    fun x ↦ ⟨(toReal.symm x, c - toReal.symm x), by simp⟩,
+    fun ⟨x, hx⟩ ↦ by ext <;> simp [← hx.out], fun x ↦ rfl⟩
+
 /-- Any subset of an antidiagonal `{(x, y) : ℝₗ × ℝₗ| x + y = c}` is a closed set. -/
-theorem isClosed_of_subset_antidiagonal {s : Set (ℝₗ × ℝₗ)} {c : ℝₗ}
-    (hs : ∀ x : ℝₗ × ℝₗ, x ∈ s → x.1 + x.2 = c) : IsClosed s := by
+theorem isClosed_of_subset_antidiagonal {s : Set (ℝₗ × ℝₗ)} {c : ℝₗ} (hs : ∀ x ∈ s, x.1 + x.2 = c) :
+    IsClosed s := by
   rw [← closure_subset_iff_isClosed]
   rintro ⟨x, y⟩ H
   obtain rfl : x + y = c := by
@@ -252,30 +259,47 @@ theorem isClosed_of_subset_antidiagonal {s : Set (ℝₗ × ℝₗ)} {c : ℝₗ
     rwa [← add_le_add_iff_left, hs _ H, add_le_add_iff_right]
 #align counterexample.sorgenfrey_line.is_closed_of_subset_antidiagonal Counterexample.SorgenfreyLine.isClosed_of_subset_antidiagonal
 
+open Subtype in
+instance (c : ℝₗ) : DiscreteTopology {x : ℝₗ × ℝₗ | x.1 + x.2 = c} :=
+  forall_open_iff_discrete.1 fun U ↦ isClosed_compl_iff.1 <| isClosed_induced_iff.2
+    ⟨val '' Uᶜ, isClosed_of_subset_antidiagonal <| coe_image_subset _ Uᶜ,
+      preimage_image_eq _ val_injective⟩
+
+/-- The Sorgenfrey plane `ℝₗ × ℝₗ` is not a normal space. -/
+theorem not_normalSpace_prod : ¬NormalSpace (ℝₗ × ℝₗ) :=
+  (isClosed_antidiagonal 0).not_normal_of_continuum_le_mk (cardinal_antidiagonal _).ge
+#align counterexample.sorgenfrey_line.not_normal_space_prod Counterexample.SorgenfreyLine.not_normalSpace_prod
+
+/-- An antidiagonal is a separable set but is not a separable space. -/
+theorem isSeparable_antidiagonal (c : ℝₗ) : IsSeparable {x : ℝₗ × ℝₗ | x.1 + x.2 = c} :=
+  isSeparable_of_separableSpace _
+
+/-- An antidiagonal is a separable set but is not a separable space. -/
+theorem not_separableSpace_antidiagonal (c : ℝₗ) :
+    ¬SeparableSpace {x : ℝₗ × ℝₗ | x.1 + x.2 = c} := by
+  rw [separableSpace_iff_countable, ← Cardinal.mk_le_aleph0_iff, cardinal_antidiagonal, not_le]
+  exact Cardinal.aleph0_lt_continuum
+
 theorem nhds_prod_antitone_basis_inv_pnat (x y : ℝₗ) :
     (𝓝 (x, y)).HasAntitoneBasis fun n : ℕ+ => Ico x (x + (n : ℝₗ)⁻¹) ×ˢ Ico y (y + (n : ℝₗ)⁻¹) := by
   rw [nhds_prod_eq]
   exact (nhds_antitone_basis_Ico_inv_pnat x).prod (nhds_antitone_basis_Ico_inv_pnat y)
 #align counterexample.sorgenfrey_line.nhds_prod_antitone_basis_inv_pnat Counterexample.SorgenfreyLine.nhds_prod_antitone_basis_inv_pnat
 
-/-- The product of the Sorgenfrey line and itself is not a normal topological space. -/
-theorem not_normalSpace_prod : ¬NormalSpace (ℝₗ × ℝₗ) := by
+/-- The sets of rational and irrational points of the antidiagonal `{(x, y) | x + y = 0}` cannot be
+separated by open neighborhoods. This implies that `ℝₗ × ℝₗ` is not a normal space. -/
+theorem not_separatedNhds_rat_irrational_antidiag :
+  ¬SeparatedNhds {x : ℝₗ × ℝₗ | x.1 + x.2 = 0 ∧ ∃ r : ℚ, ↑r = x.1}
+    {x : ℝₗ × ℝₗ | x.1 + x.2 = 0 ∧ Irrational (toReal x.1)} := by
   have h₀ : ∀ {n : ℕ+}, 0 < (n : ℝ)⁻¹ := inv_pos.2 (Nat.cast_pos.2 (PNat.pos _))
   have h₀' : ∀ {n : ℕ+} {x : ℝ}, x < x + (n : ℝ)⁻¹ := lt_add_of_pos_right _ h₀
-  intro
   /- Let `S` be the set of points `(x, y)` on the line `x + y = 0` such that `x` is rational.
     Let `T` be the set of points `(x, y)` on the line `x + y = 0` such that `x` is irrational.
     These sets are closed, see `SorgenfreyLine.isClosed_of_subset_antidiagonal`, and disjoint. -/
   set S := {x : ℝₗ × ℝₗ | x.1 + x.2 = 0 ∧ ∃ r : ℚ, ↑r = x.1}
   set T := {x : ℝₗ × ℝₗ | x.1 + x.2 = 0 ∧ Irrational (toReal x.1)}
-  have hSc : IsClosed S := isClosed_of_subset_antidiagonal fun x hx => hx.1
-  have hTc : IsClosed T := isClosed_of_subset_antidiagonal fun x hx => hx.1
-  have hd : Disjoint S T := by
-    rw [disjoint_iff_inf_le]
-    rintro ⟨x, y⟩ ⟨⟨-, r, rfl : _ = x⟩, -, hr⟩
-    exact r.not_irrational hr
   -- Consider disjoint open sets `U ⊇ S` and `V ⊇ T`.
-  rcases normal_separation hSc hTc hd with ⟨U, V, Uo, Vo, SU, TV, UV⟩
+  rintro ⟨U, V, Uo, Vo, SU, TV, UV⟩
   /- For each point `(x, -x) ∈ T`, choose a neighborhood
     `Ico x (x + k⁻¹) ×ˢ Ico (-x) (-x + k⁻¹) ⊆ V`. -/
   have : ∀ x : ℝₗ, Irrational (toReal x) →
@@ -316,7 +340,6 @@ theorem not_normalSpace_prod : ¬NormalSpace (ℝₗ × ℝₗ) := by
   · refine' (nhds_antitone_basis_Ico_inv_pnat (-x)).2 hnN ⟨neg_le_neg hxn.1.le, _⟩
     simp only [add_neg_lt_iff_le_add', lt_neg_add_iff_add_lt]
     exact hxn.2
-#align counterexample.sorgenfrey_line.not_normal_space_prod Counterexample.SorgenfreyLine.not_normalSpace_prod
 
 /-- Topology on the Sorgenfrey line is not metrizable. -/
 theorem not_metrizableSpace : ¬MetrizableSpace ℝₗ := by

Mathlib.lean

@@ -3277,6 +3277,7 @@ import Mathlib.Topology.Perfect
 import Mathlib.Topology.QuasiSeparated
 import Mathlib.Topology.Semicontinuous
 import Mathlib.Topology.Separation
+import Mathlib.Topology.Separation.NotNormal
 import Mathlib.Topology.Sequences
 import Mathlib.Topology.Sets.Closeds
 import Mathlib.Topology.Sets.Compacts

Mathlib/Topology/ContinuousFunction/Basic.lean

@@ -99,6 +99,8 @@ theorem toFun_eq_coe {f : C(α, β)} : f.toFun = (f : α → β) :=
   rfl
 #align continuous_map.to_fun_eq_coe ContinuousMap.toFun_eq_coe
 
+instance : CanLift (α → β) C(α, β) FunLike.coe Continuous := ⟨fun f hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩
+
 /-- See note [custom simps projection]. -/
 def Simps.apply (f : C(α, β)) : α → β := f
 
@@ -383,6 +385,11 @@ theorem restrict_apply_mk (f : C(α, β)) (s : Set α) (x : α) (hx : x ∈ s) :
   rfl
 #align continuous_map.restrict_apply_mk ContinuousMap.restrict_apply_mk
 
+theorem injective_restrict [T2Space β] {s : Set α} (hs : Dense s) :
+    Injective (restrict s : C(α, β) → C(s, β)) := fun f g h ↦
+  FunLike.ext' <| f.continuous.ext_on hs g.continuous <| Set.restrict_eq_restrict_iff.1 <|
+    congr_arg FunLike.coe h
+
 /-- The restriction of a continuous map to the preimage of a set. -/
 @[simps]
 def restrictPreimage (f : C(α, β)) (s : Set β) : C(f ⁻¹' s, s) :=

Mathlib/Topology/Separation/NotNormal.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2023 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Data.Real.Cardinality
+import Mathlib.Topology.Separation
+import Mathlib.Topology.TietzeExtension
+/-!
+# Not normal topological spaces
+
+In this file we prove (see `IsClosed.not_normal_of_continuum_le_mk`) that a separable space with a
+discrete subspace of cardinality continuum is not a normal topological space.
+-/
+
+open Set Function Cardinal Topology TopologicalSpace
+
+universe u
+variable {X : Type u} [TopologicalSpace X] [SeparableSpace X]
+
+/-- Let `s` be a closed set in a separable normal space. If the induced topology on `s` is discrete,
+then `s` has cardinality less than continuum.
+
+The proof follows
+https://en.wikipedia.org/wiki/Moore_plane#Proof_that_the_Moore_plane_is_not_normal -/
+theorem IsClosed.mk_lt_continuum [NormalSpace X] {s : Set X} (hs : IsClosed s)
+    [DiscreteTopology s] : #s < 𝔠 := by
+  -- Proof by contradiction: assume `𝔠 ≤ #s`
+  by_contra' h
+  -- Choose a countable dense set `t : Set X`
+  rcases exists_countable_dense X with ⟨t, htc, htd⟩
+  haveI := htc.to_subtype
+  -- To obtain a contradiction, we will prove `2 ^ 𝔠 ≤ 𝔠`.
+  refine (Cardinal.cantor 𝔠).not_le ?_
+  calc
+    -- Any function `s → ℝ` is continuous, hence `2 ^ 𝔠 ≤ #C(s, ℝ)`
+    2 ^ 𝔠 ≤ #C(s, ℝ) := by
+      rw [(ContinuousMap.equivFnOfDiscrete _ _).cardinal_eq, mk_arrow, mk_real, lift_continuum,
+        lift_uzero]
+      exact (power_le_power_left two_ne_zero h).trans (power_le_power_right (nat_lt_continuum 2).le)
+    -- By the Tietze Extension Theorem, any function `f : C(s, ℝ)` can be extended to `C(X, ℝ)`,
+    -- hence `#C(s, ℝ) ≤ #C(X, ℝ)`
+    _ ≤ #C(X, ℝ) := by
+      choose f hf using (ContinuousMap.exists_restrict_eq_of_closed · hs)
+      have hfi : Injective f := LeftInverse.injective hf
+      exact mk_le_of_injective hfi
+    -- Since `t` is dense, restriction `C(X, ℝ) → C(t, ℝ)` is injective, hence `#C(X, ℝ) ≤ #C(t, ℝ)`
+    _ ≤ #C(t, ℝ) := mk_le_of_injective <| ContinuousMap.injective_restrict htd
+    _ ≤ #(t → ℝ) := mk_le_of_injective FunLike.coe_injective
+    -- Since `t` is countable, we have `#(t → ℝ) ≤ 𝔠`
+    _ ≤ 𝔠 := by
+      rw [mk_arrow, mk_real, lift_uzero, lift_continuum, continuum, ← power_mul]
+      exact power_le_power_left two_ne_zero mk_le_aleph0
+
+/-- Let `s` be a closed set in a separable space. If the induced topology on `s` is discrete and `s`
+has cardinality at least continuum, then the ambient space is not a normal space. -/
+theorem IsClosed.not_normal_of_continuum_le_mk {s : Set X} (hs : IsClosed s) [DiscreteTopology s]
+    (hmk : 𝔠 ≤ #s) : ¬NormalSpace X := fun _ ↦ hs.mk_lt_continuum.not_le hmk