secondCountable_of_sigmaCompact — Mathlib

English

There exists a subset t ⊆ s such that t is countable and s = closure t.

Русский

Существует подмножество t ⊆ s, содержащее счетные элементы, для которого s равно closure t.

LaTeX

$$∃ t ⊆ s, t.Countable ∧ s = closure t$$

Lean4

/-- A sigma compact pseudo emetric space has second countable topology. -/
instance (priority := 90) secondCountable_of_sigmaCompact [SigmaCompactSpace α] : SecondCountableTopology α :=
  by
  suffices SeparableSpace α by exact UniformSpace.secondCountable_of_separable α
  choose T _ hTc hsubT using fun n => subset_countable_closure_of_compact (isCompact_compactCovering α n)
  refine ⟨⟨⋃ n, T n, countable_iUnion hTc, fun x => ?_⟩⟩
  rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering α) x with ⟨n, hn⟩
  exact closure_mono (subset_iUnion _ n) (hsubT _ hn)

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