isCompact_sigma — Mathlib

English

Let X_i be spaces, s a finite set of indices, and t_i compact for each i in s; then the sigma-product s.sigma t is compact.

Русский

Пусть X_i --- пространства, s конечны по индексу, и t_i компактны для каждого i ∈ s; тогда s.sigma t компактно.

LaTeX

$$$\text{hs} : s.Finite \to (\forall i \in s, \IsCompact (t_i)) \Rightarrow \IsCompact (s.sigma t)$$$

Lean4

theorem isCompact_sigma {X : ι → Type*} [∀ i, TopologicalSpace (X i)] {s : Set ι} {t : ∀ i, Set (X i)} (hs : s.Finite)
    (ht : ∀ i ∈ s, IsCompact (t i)) : IsCompact (s.sigma t) :=
  by
  rw [Set.sigma_eq_biUnion]
  exact hs.isCompact_biUnion fun i hi ↦ (ht i hi).image continuous_sigmaMk

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