English
Applying a map to the first coordinate inside image₂ is the same as applying the map to the result: image₂ f (s.image g) t = image₂ (λ a b. f (g a) b) s t.
Русский
Применение отображения к первой координате внутри image₂ эквивалентно применению отображения к результату: image₂ f (s.image g) t = image₂ (λ a b. f (g a) b) s t.
LaTeX
$$$\mathrm{image}_2\ f (\mathrm{image}\ g\ s)\ t = \mathrm{image}_2\ (\lambda a\ b. f (g\ a)\ b)\ s\ t$$$
Lean4
theorem image₂_image_left (f : γ → β → δ) (g : α → γ) : image₂ f (s.image g) t = image₂ (fun a b => f (g a) b) s t :=
coe_injective <| by
push_cast
exact image2_image_left _ _