countable_of_discrete — Mathlib

English

If X has the discrete topology and s is Lindelöf, then s is countable.

Русский

Если X имеет дискретную топологию и s — Линдельоф, то s счётно.

LaTeX

$$$[DiscreteTopology X] (IsLindelof\,s) \Rightarrow s.Countable$$$

Lean4

theorem countable_of_discrete [DiscreteTopology X] (hs : IsLindelof s) : s.Countable :=
  by
  have : ∀ x : X, ({ x } : Set X) ∈ 𝓝 x := by simp [nhds_discrete]
  rcases hs.elim_nhds_subcover (fun x => { x }) fun x _ => this x with ⟨t, ht, _, hssubt⟩
  rw [biUnion_of_singleton] at hssubt
  exact ht.mono hssubt

Похожие утверждения