isCompact_iff_of_isClosed — Mathlib

English

If s is closed in the product, then IsCompact s holds iff all coordinate projections of s are compact.

Русский

Если s замкнуто в произведении, то компактность s эквивалентна компактности всех проекций s на координатах.

LaTeX

$$$\IsClosed(s) \Rightarrow \IsCompact(s) \iff \forall i, \IsCompact(\mathrm{eval}_i'' s)$$$

Lean4

theorem isCompact_iff_of_isClosed {s : Set (Π i, X i)} (hs : IsClosed s) : IsCompact s ↔ ∀ i, IsCompact (eval i '' s) :=
  by
  constructor <;> intro H
  · exact fun i ↦ H.image <| continuous_apply i
  · exact IsCompact.of_isClosed_subset (isCompact_univ_pi H) hs (subset_pi_eval_image univ s)

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