English
Membership in map₂ is equivalent to existence of suitable witnesses: u ∈ map₂ m f g iff ∃ s ∈ f, ∃ t ∈ g, image2 m s t ⊆ u.
Русский
Членство в map₂ эквивалентно существованию подходящих свидетелей: u ∈ map₂ m f g ⇔ ∃ s ∈ f, ∃ t ∈ g, image2 m s t ⊆ u.
LaTeX
$$$u \\in \\mathrm{map\\_2}(m,f,g) \\iff \\exists s \\in f, \\exists t \\in g, \\mathrm{image2}\\; m\\; s\\; t \\subseteq u$$$
Lean4
/-- The image of a binary function `m : α → β → γ` as a function `Filter α → Filter β → Filter γ`.
Mathematically this should be thought of as the image of the corresponding function `α × β → γ`. -/
def map₂ (m : α → β → γ) (f : Filter α) (g : Filter β) : Filter γ :=
((f ×ˢ g).map (uncurry m)).copy {s | ∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s} fun _ ↦ by
simp only [mem_map, mem_prod_iff, image2_subset_iff, prod_subset_iff]; rfl
