feat(Topology/Separation/NotNormal): generalize to non-separable spaces (#33414)

Author: peakpoint

Counterexamples/SorgenfreyLine.lean

@@ -3,15 +3,14 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import Mathlib.Analysis.Real.Cardinality
 import Mathlib.Order.Interval.Set.Monotone
+import Mathlib.Topology.Baire.Lemmas
+import Mathlib.Topology.Baire.LocallyCompactRegular
+import Mathlib.Topology.EMetricSpace.Paracompact
 import Mathlib.Topology.Instances.Irrational
-import Mathlib.Topology.Algebra.Order.Archimedean
-import Mathlib.Topology.Compactness.Paracompact
 import Mathlib.Topology.Metrizable.Urysohn
-import Mathlib.Topology.EMetricSpace.Paracompact
 import Mathlib.Topology.Separation.NotNormal
-import Mathlib.Topology.Baire.Lemmas
-import Mathlib.Topology.Baire.LocallyCompactRegular
 
 /-!
 # Sorgenfrey line

Mathlib/Topology/Separation/NotNormal.lean

@@ -1,61 +1,78 @@
 /-
 Copyright (c) 2023 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yury Kudryashov
+Authors: Yury Kudryashov, Tian Chen
 -/
 module
 
-public import Mathlib.Analysis.Real.Cardinality
-public import Mathlib.Topology.TietzeExtension
+public import Mathlib.SetTheory.Cardinal.Continuum
+public import Mathlib.Topology.Separation.Regular
+
 /-!
 # 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.
+
+## References
+
+* [Willard's *General Topology*][zbMATH02107988]
 -/
 
 public section
 
-open Set Function Cardinal Topology TopologicalSpace
+open Set Function Cardinal TopologicalSpace
 
 universe u
-variable {X : Type u} [TopologicalSpace X] [SeparableSpace X]
+variable {X : Type u} [TopologicalSpace 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_ge ?_
+namespace IsClosed
+
+/-- Let `s` be a closed set in a normal space and `d` be a dense set. If the induced topology on `s`
+is discrete, then `𝒫 s` has cardinality less than or equal to `𝒫 d`. -/
+theorem two_pow_mk_le_two_pow_mk_dense [NormalSpace X] {s d : Set X} (hs : IsClosed s)
+    [DiscreteTopology s] (hd : Dense d) : (2 : Cardinal) ^ #s ≤ 2 ^ #d := by
+  have h_closed (t) (ht : t ∈ 𝒫 s) : IsClosed t := by
+    rw [← inter_eq_self_of_subset_right ht, ← Subtype.image_preimage_val]
+    exact hs.isClosedMap_subtype_val _ (isClosed_discrete _)
+  choose U V hU hV hUs hVs hUV using fun t : 𝒫 s ↦
+    normal_separation (h_closed t t.2) (h_closed _ diff_subset) disjoint_sdiff_right
+  have hUd {t₁ t₂} (h : U t₁ ∩ d = U t₂ ∩ d) : t₁.1 ⊆ t₂.1 := by
+    by_contra ht
+    rw [← diff_nonempty] at ht
+    have hUVd := hd.inter_open_nonempty _ ((hU t₁).inter (hV t₂)) <| ht.mono <|
+      subset_inter (diff_subset.trans (hUs t₁)) ((diff_subset_diff_left t₁.2).trans (hVs t₂))
+    rw [inter_right_comm, h] at hUVd
+    exact hUVd.not_disjoint <| disjoint_of_subset_left inter_subset_left (hUV t₂)
+  have h_inj : Injective (U · ∩ d) := fun _ _ h ↦ SetCoe.ext <| (hUd h).antisymm (hUd h.symm)
+  rw [← mk_powerset, ← mk_powerset, ← mk_range_eq _ h_inj]
+  apply mk_le_mk_of_subset
+  rw [range_subset_iff]
+  intro
+  exact inter_subset_right
+
+theorem mk_lt_two_pow_mk_dense [NormalSpace X] {s d : Set X} (hs : IsClosed s)
+    [DiscreteTopology s] (hd : Dense d) : #s < 2 ^ #d :=
+  (#s).cantor.trans_le <| hs.two_pow_mk_le_two_pow_mk_dense hd
+
+variable [SeparableSpace X]
+
+theorem two_pow_mk_lt_continuum [NormalSpace X] {s : Set X} (hs : IsClosed s)
+    [DiscreteTopology s] : 2 ^ #s ≤ 𝔠 :=
+  have ⟨d, hd_countable, hd_dense⟩ := exists_countable_dense X
   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 (Y := ℝ) 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 DFunLike.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
+    2 ^ #s ≤ 2 ^ #d := hs.two_pow_mk_le_two_pow_mk_dense hd_dense
+    _ ≤ 2 ^ ℵ₀ := power_le_power_left two_ne_zero hd_countable.le_aleph0
+    _ = 𝔠 := two_power_aleph0
+
+/-- 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. -/
+theorem mk_lt_continuum [NormalSpace X] {s : Set X} (hs : IsClosed s)
+  [DiscreteTopology s] : #s < 𝔠 := (#s).cantor.trans_le hs.two_pow_mk_lt_continuum
 
 /-- 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]
+theorem not_normal_of_continuum_le_mk {s : Set X} (hs : IsClosed s) [DiscreteTopology s]
     (hmk : 𝔠 ≤ #s) : ¬NormalSpace X := fun _ ↦ hs.mk_lt_continuum.not_ge hmk
+
+end IsClosed