English
The coproduct of cocompact filters on a family of spaces equals the cocompact filter on the product space.
Русский
Копродукт кокопомпакт-фильтров по семейству пространств равен кокопомпакт-фильтру их произведения.
LaTeX
$$$\text{Filter.coprodᵢ}(\lambda d, \text{Filter.cocompact}(X_d)) = \text{Filter.cocompact}(\prod_d X_d)$$$
Lean4
/-- **Tychonoff's theorem** formulated in terms of filters: `Filter.cocompact` on an indexed product
type `Π d, X d` the `Filter.coprodᵢ` of filters `Filter.cocompact` on `X d`. -/
theorem coprodᵢ_cocompact {X : ι → Type*} [∀ d, TopologicalSpace (X d)] :
(Filter.coprodᵢ fun d => Filter.cocompact (X d)) = Filter.cocompact (∀ d, X d) :=
by
refine le_antisymm (iSup_le fun i => Filter.comap_cocompact_le (continuous_apply i)) ?_
refine compl_surjective.forall.2 fun s H => ?_
simp only [compl_mem_coprodᵢ, Filter.mem_cocompact, compl_subset_compl, image_subset_iff] at H ⊢
choose K hKc htK using H
exact ⟨Set.pi univ K, isCompact_univ_pi hKc, fun f hf i _ => htK i hf⟩
