English
For a product of spaces, a subset is compact if and only if it is closed and all coordinate projections have compact images.
Русский
Для произведения пространств множество компактности эквивалентно тому, чтобы множество было замкнуто и образ каждого координатного проектора компактен.
LaTeX
$$$IsCompact s \\iff IsClosed s \\land \\forall i, IsCompact (eval_i'' s).$$$
Lean4
theorem isCompact_iff {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, T2Space (X i)]
{s : Set (Π i, X i)} : IsCompact s ↔ IsClosed s ∧ ∀ i, IsCompact (eval i '' s) :=
by
constructor <;> intro H
· exact ⟨H.isClosed, fun i ↦ H.image <| continuous_apply i⟩
· exact IsCompact.of_isClosed_subset (isCompact_univ_pi H.2) H.1 (subset_pi_eval_image univ s)
