English
Another articulation of the triple-image₂ commutativity under a correspondence condition between the four maps.
Русский
Еще одно выражение тройной совместимости образа₂ при условии соответствия между четырьмя отображениями.
LaTeX
$$$\forall a,b,c,d,\ f (g a b) (h c d) = f' (g' a c) (h' b d) \Rightarrow \mathrm{image}_2 f (\mathrm{image}_2 g s t) (\mathrm{image}_2 h u v) = \mathrm{image}_2 f' (\mathrm{image}_2 g' s u) (\mathrm{image}_2 h' t v)$$$
Lean4
theorem image₂_image₂_image₂_comm {γ δ : Type*} {u : Finset γ} {v : Finset δ} [DecidableEq ζ] [DecidableEq ζ']
[DecidableEq ν] {f : ε → ζ → ν} {g : α → β → ε} {h : γ → δ → ζ} {f' : ε' → ζ' → ν} {g' : α → γ → ε'}
{h' : β → δ → ζ'} (h_comm : ∀ a b c d, f (g a b) (h c d) = f' (g' a c) (h' b d)) :
image₂ f (image₂ g s t) (image₂ h u v) = image₂ f' (image₂ g' s u) (image₂ h' t v) :=
coe_injective <| by
push_cast
exact image2_image2_image2_comm h_comm
