English
For spaces indexed by ι with a Pi-topology, a subset of the product has a compact superset iff each coordinate projection has a compact superset.
Русский
Для пространства, индексируемого по ι, с топологией Пи, подмножество произведения имеет компактное надмножество тогда и только тогда, когда каждое прокоэр множеств имеет компактное надмножество.
LaTeX
$$$\text{Exists } K: IsCompact K \land s \subseteq K \iff \forall i, \exists Ki, IsCompact Ki \land s \subseteq \mathrm{eval}_i^{-1}(Ki)$$$
Lean4
/-- **Tychonoff's theorem**: product of compact sets is compact. -/
theorem isCompact_pi_infinite {s : ∀ i, Set (X i)} :
(∀ i, IsCompact (s i)) → IsCompact {x : ∀ i, X i | ∀ i, x i ∈ s i} :=
by
simp only [isCompact_iff_ultrafilter_le_nhds, nhds_pi, le_pi, le_principal_iff]
intro h f hfs
have : ∀ i : ι, ∃ x, x ∈ s i ∧ Tendsto (Function.eval i) f (𝓝 x) :=
by
refine fun i => h i (f.map _) (mem_map.2 ?_)
exact mem_of_superset hfs fun x hx => hx i
choose x hx using this
exact ⟨x, fun i => (hx i).left, fun i => (hx i).right⟩
