[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
⊢ #↑s < 𝔠
[PROOFSTEP]
by_contra' h
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
⊢ False
[PROOFSTEP]
rcases exists_countable_dense X with ⟨t, htc, htd⟩
[GOAL]
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
⊢ False
[PROOFSTEP]
haveI := htc.to_subtype
[GOAL]
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ False
[PROOFSTEP]
refine (Cardinal.cantor 𝔠).not_le ?_
[GOAL]
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ 2 ^ 𝔠 ≤ 𝔠
[PROOFSTEP]
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
  _ ≤ #C(t, ℝ) := (mk_le_of_injective <| ContinuousMap.injective_restrict htd)
  _ ≤ #(t → ℝ) := (mk_le_of_injective FunLike.coe_injective)
  _ ≤ 𝔠 := by
    rw [mk_arrow, mk_real, lift_uzero, lift_continuum, continuum, ← power_mul]
    exact power_le_power_left two_ne_zero mk_le_aleph0
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ 2 ^ 𝔠 ≤ #C(↑s, ℝ)
[PROOFSTEP]
rw [(ContinuousMap.equivFnOfDiscrete _ _).cardinal_eq, mk_arrow, mk_real, lift_continuum, lift_uzero]
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ 2 ^ 𝔠 ≤ 𝔠 ^ #↑s
[PROOFSTEP]
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, ℝ)`
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ #C(↑s, ℝ) ≤ #C(X, ℝ)
[PROOFSTEP]
choose f hf using (ContinuousMap.exists_restrict_eq_of_closed · hs)
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
f : C(↑s, ℝ) → C(X, ℝ)
hf : ∀ (x : C(↑s, ℝ)), ContinuousMap.restrict s (f x) = x
⊢ #C(↑s, ℝ) ≤ #C(X, ℝ)
[PROOFSTEP]
have hfi : Injective f := LeftInverse.injective hf
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
f : C(↑s, ℝ) → C(X, ℝ)
hf : ∀ (x : C(↑s, ℝ)), ContinuousMap.restrict s (f x) = x
hfi : Injective f
⊢ #C(↑s, ℝ) ≤ #C(X, ℝ)
[PROOFSTEP]
exact mk_le_of_injective hfi
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ #(↑t → ℝ) ≤ 𝔠
[PROOFSTEP]
rw [mk_arrow, mk_real, lift_uzero, lift_continuum, continuum, ← power_mul]
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ 2 ^ (ℵ₀ * #↑t) ≤ 2 ^ ℵ₀
[PROOFSTEP]
exact power_le_power_left two_ne_zero mk_le_aleph0
