English
The coproduct of cocompact filters on two spaces equals the cocompact filter on their product.
Русский
Копродукт кокопомпакт-фильтров двух пространств равен кокопомпакт-фильтру их произведения.
LaTeX
$$$\Filter.cocompact(X) \coprod \Filter.cocompact(Y) = \Filter.cocompact(X \times Y)$$$
Lean4
/-- The coproduct of the cocompact filters on two topological spaces is the cocompact filter on
their product. -/
theorem coprod_cocompact : (Filter.cocompact X).coprod (Filter.cocompact Y) = Filter.cocompact (X × Y) :=
by
apply le_antisymm
· exact sup_le (comap_cocompact_le continuous_fst) (comap_cocompact_le continuous_snd)
· refine (hasBasis_cocompact.coprod hasBasis_cocompact).ge_iff.2 fun K hK ↦ ?_
rw [← univ_prod, ← prod_univ, ← compl_prod_eq_union]
exact (hK.1.prod hK.2).compl_mem_cocompact
