English
For any map m : α × β → γ and filters f on α and g on β, the image of a product filter under m equals the sequential composition of the image of f under the curried map with g; specifically map m (f ×ˢ g) = (f.map (λ a,b, m(a,b))).seq g.
Русский
Для отображения m: α × β → γ и фильтров f на α и g на β выполняется равенство: map m (f ×ˢ g) = (f.map (λ(a,b), m(a,b))).seq g.
LaTeX
$$$ \\operatorname{map}(m)\\bigl(f \\times g\\bigr) = \\bigl(f.\\operatorname{map}(\\lambda a,b. m(a,b))\\bigr).\\mathrm{seq}\\ g $$$
Lean4
protected theorem map_prod (m : α × β → γ) (f : Filter α) (g : Filter β) :
map m (f ×ˢ g) = (f.map fun a b => m (a, b)).seq g :=
by
simp only [Filter.ext_iff, mem_map, mem_prod_iff, mem_map_seq_iff, exists_and_left]
intro s
constructor
· exact fun ⟨t, ht, s, hs, h⟩ => ⟨s, hs, t, ht, fun x hx y hy => @h ⟨x, y⟩ ⟨hx, hy⟩⟩
· exact fun ⟨s, hs, t, ht, h⟩ => ⟨t, ht, s, hs, fun ⟨x, y⟩ ⟨hx, hy⟩ => h x hx y hy⟩
