secondCountable_of_sigmaCompact — Mathlib

English

If H is second-countable and M is sigma-compact, then M is second-countable.

Русский

Если H вторично счётно, а M сигма-компактно, то M тоже вторично счётно.

LaTeX

$$$[\text{SecondCountableTopology } H] \;[\Sigma\text{-compactSpace } M] \Rightarrow \text{SecondCountableTopology } M$$$

Lean4

theorem secondCountable_of_sigmaCompact [SecondCountableTopology H] [SigmaCompactSpace M] : SecondCountableTopology M :=
  by
  obtain ⟨s, hsc, hsU⟩ : ∃ s, Set.Countable s ∧ ⋃ (x) (_ : x ∈ s), (chartAt H x).source = univ :=
    countable_cover_nhds_of_sigmaCompact fun x : M ↦ chart_source_mem_nhds H x
  exact ChartedSpace.secondCountable_of_countable_cover H hsU hsc

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