English
The binary image of a function m is extended to filters: map₂ m f g is the filter generated by all image2 m s t with s ∈ f and t ∈ g.
Русский
Бинарное отображение функции m расширено до фильтров: map₂ m f g порождает фильтр порожденный всеми image2 m s t с s ∈ f и t ∈ g.
LaTeX
$$$\\mathrm{map\\_2}\\; m\\; f\\; g = \\text{(construction described in def)}$$$
Lean4
@[simp]
theorem map₂_mk_eq_prod (f : Filter α) (g : Filter β) : map₂ Prod.mk f g = f ×ˢ g := by
simp only [← map_prod_eq_map₂, map_id']
-- lemma image2_mem_map₂_iff (hm : injective2 m) : image2 m s t ∈ map₂ m f g ↔ s ∈ f ∧ t ∈ g :=
-- ⟨by { rintro ⟨u, v, hu, hv, h⟩, rw image2_subset_image2_iff hm at h,
-- exact ⟨mem_of_superset hu h.1, mem_of_superset hv h.2⟩ }, fun h ↦ image2_mem_map₂ h.1 h.2⟩
