English
If h_distrib: ∀ a b c, f a (g b c) = g'(f1 a b) (f2 a c) holds, then image2 f s (image2 g t u) ⊆ image2 g' (image2 f1 s t) (image2 f2 s u).
Русский
Если выполняется условие распределения h_distrib: f a (g b c) = g'(f1 a b) (f2 a c), то image2 f s (image2 g t u) ⊆ image2 g' (image2 f1 s t) (image2 f2 s u).
LaTeX
$$$\\forall a b c,\\ f(a, g(b,c)) = g'(f1(a,b), f2(a,c)) \\Rightarrow image2 f s (image2 g t u) \\subseteq image2 g' (image2 f1 s t) (image2 f2 s u)$$$
Lean4
/-- The other direction does not hold because of the `u`-`u` cross terms on the RHS. -/
theorem image2_distrib_subset_right {f : δ → γ → ε} {g : α → β → δ} {f₁ : α → γ → α'} {f₂ : β → γ → β'}
{g' : α' → β' → ε} (h_distrib : ∀ a b c, f (g a b) c = g' (f₁ a c) (f₂ b c)) :
image2 f (image2 g s t) u ⊆ image2 g' (image2 f₁ s u) (image2 f₂ t u) := by grind
