English
The coproduct of principal filters equals the principal filter generated by the de Morgan form of the cross product of complements.
Русский
Копродукт главных фильтров равен главному фильтру, порождённому формой де Моргана над пересечением дополнений.
LaTeX
$$$ (\mathcal P s).coprod (\mathcal P t) = \mathcal P\big((s^{c} \times t^{c})^{c}\big). $$$
Lean4
theorem principal_coprod_principal (s : Set α) (t : Set β) : (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ := by
rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter, preimage_compl,
preimage_compl, compl_compl, compl_compl]
-- this inequality can be strict; see `map_const_principal_coprod_map_id_principal` and
-- `map_prodMap_const_id_principal_coprod_principal` below.
