sigmaCompactSpace_of_locallyCompact_secondCountable

English

Locally compact and second countable spaces are σ-compact.

Русский

Локально компактное пространство и счетное по базису пространство являются σ-компактными.

LaTeX

$$$LocallyCompactSpace X \\wedge SecondCountableTopology X \\rightarrow SigmaCompactSpace X$$$

Lean4

instance (priority := 100) sigmaCompactSpace_of_locallyCompact_secondCountable [LocallyCompactSpace X]
    [SecondCountableTopology X] : SigmaCompactSpace X :=
  by
  choose K hKc hxK using fun x : X => exists_compact_mem_nhds x
  rcases countable_cover_nhds hxK with ⟨s, hsc, hsU⟩
  refine SigmaCompactSpace.of_countable _ (hsc.image K) (forall_mem_image.2 fun x _ => hKc x) ?_
  rwa [sUnion_image]

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