instSigmaCompactSpaceForallOfFinite

English

A compact space is σ-compact.

Русский

Компактное пространство σ-компактно.

LaTeX

$$$CompactSpace X \\rightarrow SigmaCompactSpace X$$$

Lean4

instance [Finite ι] {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, SigmaCompactSpace (X i)] :
    SigmaCompactSpace (∀ i, X i) :=
  by
  refine
    ⟨⟨fun n => Set.pi univ fun i => compactCovering (X i) n, fun n =>
        isCompact_univ_pi fun i => isCompact_compactCovering (X i) _, ?_⟩⟩
  rw [iUnion_univ_pi_of_monotone]
  · simp only [iUnion_compactCovering, pi_univ]
  · exact fun i => compactCovering_subset (X i)

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