English
If a,b,c satisfy a compatibility relation, then image₂ f (image₂ g s t) u = image₂ f' s (image₂ g' t u).
Русский
Если тождественные отношения между f,g и f',g' выполняются, то образ₂ ассоциируется: image₂ f (image₂ g s t) u = image₂ f' s (image₂ g' t u).
LaTeX
$$$\forall a,b,c,\ f(g(a,b),c) = f'(a,g'(b,c)) \Rightarrow \mathrm{image}_2 f (\mathrm{image}_2 g s t) u = \mathrm{image}_2 f' s (\mathrm{image}_2 g' t u)$$$
Lean4
theorem image₂_right_comm {γ : Type*} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε}
(h_right_comm : ∀ a b c, f (g a b) c = g' (f' a c) b) : image₂ f (image₂ g s t) u = image₂ g' (image₂ f' s u) t :=
coe_injective <| by
push_cast
exact image2_right_comm h_right_comm
