English
Every compact subset of a sigma-product can be represented as a finite sigma-coordinate product: there exist a finite set s of indices and compact sets t_i such that s.sigma t equals the given compact set.
Русский
Каждое компактное подмножество сигма-производного может быть выражено как конечное σ-координатное произведение: существует конечное множество индексов s и компактные множества t_i такие, что s.sigma t равно данному компактному множеству.
LaTeX
$$$\exists s\;\exists t, s.Finite \\land (\forall i, \IsCompact (t_i)) \\land s.sigma t = u$$$
Lean4
theorem sigma_exists_finite_sigma_eq {X : ι → Type*} [∀ i, TopologicalSpace (X i)] (u : Set (Σ i, X i))
(hu : IsCompact u) : ∃ (s : Set ι) (t : ∀ i, Set (X i)), s.Finite ∧ (∀ i, IsCompact (t i)) ∧ s.sigma t = u :=
by
obtain ⟨s, hs⟩ :=
hu.elim_finite_subcover (fun i : ι ↦ Sigma.mk i '' (Sigma.mk i ⁻¹' Set.univ))
(fun i ↦ isOpenMap_sigmaMk _ <| isOpen_univ.preimage continuous_sigmaMk) fun x hx ↦ (by simp)
use s, fun i ↦ Sigma.mk i ⁻¹' u, s.finite_toSet, fun i ↦ ?_, ?_
· exact Topology.IsClosedEmbedding.sigmaMk.isCompact_preimage hu
· ext x
simp only [Set.mem_sigma_iff, Finset.mem_coe, Set.mem_preimage, and_iff_right_iff_imp]
intro hx
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (hs hx)
simp_all
