instCompactSpaceProd — Mathlib

English

The product of compact spaces is compact: if each X_i is compact, then the product ∏ i X_i is compact.

Русский

Тайконов: произведение компактых пространств компактно: если каждый X_i компактен, то их произведение компактно.

LaTeX

$$$\forall i, \IsCompact (X_i) \Rightarrow \IsCompact(\prod_i X_i)$$$

Lean4

/-- The product of two compact spaces is compact. -/
instance [CompactSpace X] [CompactSpace Y] : CompactSpace (X × Y) :=
  ⟨by rw [← univ_prod_univ]; exact isCompact_univ.prod isCompact_univ⟩

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