English
Symmetric statement image2_image2_comm: if h_comm holds for all a,b,c,d then image2 f (image2 g s t) (image2 h u v) = image2 f' (image2 g' s u) (image2 h' t v).
Русский
Симметричное свойство для тройного изображения: если выполняется равенство-правило для всех a,b,c,d, то image2 f (image2 g s t) (image2 h u v) = image2 f' (image2 g' s u) (image2 h' t v).
LaTeX
$$$\\forall a b c d:\\ (h\\_comm\\ a\\ b\\ c\\ d) \\Rightarrow \\operatorname{image}_2 f (\\operatorname{image}_2 g s t) (\\operatorname{image}_2 h u v) = \\operatorname{image}_2 f' (\\operatorname{image}_2 g' s u) (\\operatorname{image}_2 h' t v)$$$
Lean4
/-- The other direction does not hold because of the `s`-`s` cross terms on the RHS. -/
theorem image2_distrib_subset_left {f : α → δ → ε} {g : β → γ → δ} {f₁ : α → β → β'} {f₂ : α → γ → γ'}
{g' : β' → γ' → ε} (h_distrib : ∀ a b c, f a (g b c) = g' (f₁ a b) (f₂ a c)) :
image2 f s (image2 g t u) ⊆ image2 g' (image2 f₁ s t) (image2 f₂ s u) := by grind
