image2_image_left — Mathlib

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

Похожие утверждения