English
For f: γ → β → δ and g: α → γ, image2 f (g '' S) T = image2 (λ a b, f (g a) b) S T.
Русский
Для f: γ → β → δ и g: α → γ имеем image2 f (g '' S) T = image2 (λ a b, f (g a) b) S T.
LaTeX
$$$$ \\operatorname{image2} f (\\operatorname{image} g S) T = \\operatorname{image2}(\\lambda a b. f (g a) b) S T. $$$$
Lean4
theorem image2_image_left (f : γ → β → δ) (g : α → γ) : image2 f (g '' s) t = image2 (fun a b => f (g a) b) s t := by
ext; simp