image₂_assoc — Mathlib

English

If for all a,b we have f a b = g b a, then image₂ f s t = image₂ g t s.

Русский

Если для всех a,b выполняется f a b = g b a, то image₂ f s t = image₂ g t s.

LaTeX

$$$\forall a,b,\ f\ a\ b = g\ b\ a \Rightarrow \mathrm{image}_2\ f\ s\ t = \mathrm{image}_2\ g\ t\ s$$$

Lean4

theorem image₂_assoc {γ : Type*} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'}
    (h_assoc : ∀ a b c, f (g a b) c = f' a (g' b c)) : image₂ f (image₂ g s t) u = image₂ f' s (image₂ g' t u) :=
  coe_injective <| by
    push_cast
    exact image2_assoc h_assoc

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