English
Let s ⊆ α and t ⊆ β. If g: β → γ is a function, then the set of all values f(a, g(b)) with a ∈ s and b ∈ t equals the image of s × t under the map (a,b) ↦ f(a, g(b)). Equivalently, image2 f s (g '' t) = image2 (λ a b, f a (g b)) s t.
Русский
Пусть s ⊆ α и t ⊆ β. Пусть g: β → γ. Тогда множество значений f(a, g(b)) при a ∈ s и b ∈ t совпадает с образом множества пар (a,b) из s×t через отображение (a,b) ↦ f(a, g(b)). То есть image2 f s (g '' t) = image2 (λ a b, f a (g b)) s t.
LaTeX
$$$\\operatorname{image}_2 f\\, s\\, (g''t) = \\operatorname{image}_2(\\lambda a\\, b.\\ f\\, a\\ (g\\, b))\\, s\\, t$$$
Lean4
theorem image2_image_right (f : α → γ → δ) (g : β → γ) : image2 f s (g '' t) = image2 (fun a b => f a (g b)) s t := by
ext; simp
