English
For spaces indexed by ι, a subset of the product has a compact superset iff for every i there exists a compact Ki with the subset contained in eval i⁻¹(Ki).
Русский
Для индексации по ι подмножество произведения имеет компактное надмножество тогда и только тогда, когда для каждого i существует компактное Ki удовлетворяющее s ⊆ eval_i^{-1}(Ki).
LaTeX
$$$\exists K \; IsCompact K \land s \subseteq K \iff \forall i, \exists Ki, IsCompact Ki \land s \subseteq \mathrm{eval}_i^{-1}' Ki$$$
Lean4
protected theorem exists_compact_superset_iff {s : Set (Π i, X i)} :
(∃ K, IsCompact K ∧ s ⊆ K) ↔ ∀ i, ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki :=
by
constructor
· intro ⟨K, hK, hsK⟩ i
exact ⟨eval i '' K, hK.image <| continuous_apply i, hsK.trans <| K.subset_preimage_image _⟩
· intro H
choose K hK hsK using H
exact ⟨pi univ K, isCompact_univ_pi hK, fun _ hx i _ ↦ hsK i hx⟩
