secondCountable_of_almost_dense_set

English

A sigma-compact pseudo-EMetric space has a second countable topology.

Русский

Сигма-компактное псевдоэметрическое пространство обладает второй счетной топологией.

LaTeX

$$SecondCountableTopology α$$

Lean4

theorem secondCountable_of_almost_dense_set (hs : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ) :
    SecondCountableTopology α :=
  by
  suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α
  have : ∀ ε > 0, ∃ t : Set α, Set.Countable t ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε := by
    simpa only [univ_subset_iff] using hs
  rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩
  exact ⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩

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