image₂_image_left — Mathlib

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 _ _

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