isCompact_univ_pi — Mathlib

English

Tychonoff’s theorem in Pi form: if each s_i is compact, then the product of univ spaces over i is compact.

Русский

Тайконовская теорема в форме Π: если каждый s_i компактен, то произведение по i пространств с незаданной верхнетопологией является компактным.

LaTeX

$$$\forall i, \IsCompact (s_i) \Rightarrow \IsCompact (\mathrm{univ}.\mathrm{pi}\ s)$$$

Lean4

/-- **Tychonoff's theorem** formulated using `Set.pi`: product of compact sets is compact. -/
theorem isCompact_univ_pi {s : ∀ i, Set (X i)} (h : ∀ i, IsCompact (s i)) : IsCompact (pi univ s) :=
  by
  convert isCompact_pi_infinite h
  simp only [← mem_univ_pi, setOf_mem_eq]

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