English
Repeat of the four-way distributive commutation: image₂ f (image₂ g s t) (image₂ h u v) = image₂ f' (image₂ g' s u) (image₂ h' t v) under the corresponding hypothesis.
Русский
Повторение четырехуровневой коммутативности образа₂.
LaTeX
$$$\text{(same as 95402 with the same assumptions)}$$$
Lean4
theorem image₂_left_comm {γ : Type*} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε}
(h_left_comm : ∀ a b c, f a (g b c) = g' b (f' a c)) : image₂ f s (image₂ g t u) = image₂ g' t (image₂ f' s u) :=
coe_injective <| by
push_cast
exact image2_left_comm h_left_comm