English
Another explicit formula showing how a coproduct of principal filters behaves under a product map when one side is constant.
Русский
Ещё одно явное выражение того, как копродукт главных фильтров ведёт себя при отображении произведения, когда одна часть константна.
LaTeX
$$$ map (Prod.map (fun _ : \alpha => b) id) ((\mathcal P { a }).coprod (\mathcal P { i })) = \mathcal P ({b} \times univ) $$$
Lean4
/-- Characterization of the `Filter.map` of the coproduct of two principal filters `𝓟 {a}` and
`𝓟 {i}`, under the `Prod.map` of two functions, respectively the constant function `fun a => b` and
the identity function. Together with the previous lemma,
`map_const_principal_coprod_map_id_principal`, this provides an example showing that the inequality
in the lemma `map_prodMap_coprod_le` can be strict. -/
theorem map_prodMap_const_id_principal_coprod_principal {α β ι : Type*} (a : α) (b : β) (i : ι) :
map (Prod.map (fun _ : α => b) id) ((𝓟 { a }).coprod (𝓟 { i })) = 𝓟 (({ b } : Set β) ×ˢ (univ : Set ι)) :=
by
rw [principal_coprod_principal, map_principal]
congr
ext ⟨b', i'⟩
constructor
· rintro ⟨⟨a'', i''⟩, _, h₂, h₃⟩
simp
· rintro ⟨h₁, _⟩
use (a, i')
simpa using h₁.symm
