English
If ι is finite and each X i is a topological space and σ-compact, then the product space (i → X i) is σ-compact.
Русский
Если индекс множество ι конечно, и каждый X_i имеет топологическое пространство и σ-компактность, то произведение пространств (i → X_i) σ-скомпактно.
LaTeX
$$$[Finite ι] \\rightarrow (\\forall i, TopologicalSpace (X i)) \\rightarrow (\\forall i, SigmaCompactSpace (X i)) \\rightarrow SigmaCompactSpace ((i : ι) \\rightarrow X i)$$$
Lean4
instance [Countable ι] {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, SigmaCompactSpace (X i)] :
SigmaCompactSpace (Σ i, X i) := by
cases isEmpty_or_nonempty ι
· infer_instance
· rcases exists_surjective_nat ι with ⟨f, hf⟩
refine ⟨⟨fun n => ⋃ k ≤ n, Sigma.mk (f k) '' compactCovering (X (f k)) n, fun n => ?_, ?_⟩⟩
· refine (finite_le_nat _).isCompact_biUnion fun k _ => ?_
exact (isCompact_compactCovering _ _).image continuous_sigmaMk
· simp only [iUnion_eq_univ_iff, Sigma.forall, mem_iUnion, hf.forall]
intro k y
rcases exists_mem_compactCovering y with ⟨n, hn⟩
refine ⟨max k n, k, le_max_left _ _, mem_image_of_mem _ ?_⟩
exact compactCovering_subset _ (le_max_right _ _) hn
