English
Let f: α × β → γ. Then the two-argument image2 of the curried form equals the image of the product set under f: { f(a,b) | a ∈ S, b ∈ T } = { f(a,b) | (a,b) ∈ S × T }.
Русский
Пусть f: α × β → γ. Тогда образ image2 (λ(a,b) . f(a,b)) по S и T совпадает с образом f от произведения S × T: { f(a,b) | a ∈ S, b ∈ T } = { f(a,b) | (a,b) ∈ S × T }.
LaTeX
$$$$\\{ f(a,b) \\mid a \\in S,\\; b \\in T \\} = \\{ f(a,b) \\mid (a,b) \\in S \\times T \\}.$$$$
Lean4
@[simp]
theorem image2_curry (f : α × β → γ) (s : Set α) (t : Set β) : image2 (fun a b ↦ f (a, b)) s t = f '' s ×ˢ t := by
simp [← image_uncurry_prod, uncurry]
