English
If X is a sigma-compact space and e: Y → X is a closed embedding, then Y is sigma-compact. In particular, there exists an increasing sequence of compact subsets K_n of Y whose union is Y, obtained as the preimages e^{-1}(C_n) of a covering X = ⋃ C_n by compact sets.
Русский
Если X является σ-компактным пространством и e: Y → X является замкнутым вложением, то Y также σ-компактно. Существуют возрастающие компактные подсемейства Y: K_n = e^{-1}(C_n), где X = ⋃ C_n (C_n компакт), и ⋃_n K_n = Y.
LaTeX
$$$$\exists (C_n)_{n\in\mathbb{N}}\,\bigl(\forall n,\ C_n \subseteq X\ \text{compact}\bigr)\land C_1 \subseteq C_2 \subseteq \cdots \land Y = \bigcup_{n\in\mathbb{N}} e^{-1}(C_n).$$$$
Lean4
protected theorem sigmaCompactSpace {e : Y → X} (he : IsClosedEmbedding e) : SigmaCompactSpace Y :=
⟨⟨fun n => e ⁻¹' compactCovering X n, fun _ => he.isCompact_preimage (isCompact_compactCovering _ _), by
rw [← preimage_iUnion, iUnion_compactCovering, preimage_univ]⟩⟩
