English
A specific instance where the map of a coproduct of principal filters under Prod.map equals the principal filter on the union of cross products.
Русский
Конкретный пример, где отображение копродукта главных фильтров находится в главном фильтре на объединении пересечённых произведений.
LaTeX
$$$ map (Prod.map (fun x => b) id) ((\mathcal P { a }).coprod (\mathcal P { i })) = \mathcal P ((\{ b \} \times univ) \cup (univ \times \{ i \})) $$$
Lean4
/-- Characterization of the coproduct of the `Filter.map`s of two principal filters `𝓟 {a}` and
`𝓟 {i}`, the first under the constant function `fun a => b` and the second under the identity
function. Together with the next lemma, `map_prodMap_const_id_principal_coprod_principal`, this
provides an example showing that the inequality in the lemma `map_prodMap_coprod_le` can be strict.
-/
theorem map_const_principal_coprod_map_id_principal {α β ι : Type*} (a : α) (b : β) (i : ι) :
(map (fun _ => b) (𝓟 { a })).coprod (map id (𝓟 { i })) =
𝓟 ((({ b } : Set β) ×ˢ univ) ∪ (univ ×ˢ ({ i } : Set ι))) :=
by simp only [map_principal, Filter.coprod, comap_principal, sup_principal, image_singleton, prod_univ, univ_prod, id]
