image₂_image_right — Mathlib

English

Similarly, image₂ f s (t.image g) = image₂ (λ a b. f a (g b)) s t.

Русский

Аналогично, image₂ f s (t.image g) = image₂ (λ a b. f a (g b)) s t.

LaTeX

$$$\mathrm{image}_2\ f\ s\ (\mathrm{image}\ g\ t) = \mathrm{image}_2\ (\lambda a b. f\ a\ (g\ b))\ s\ t$$$

Lean4

theorem image₂_image_right (f : α → γ → δ) (g : β → γ) : image₂ f s (t.image g) = image₂ (fun a b => f a (g b)) s t :=
  coe_injective <| by
    push_cast
    exact image2_image_right _ _

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