English
Let γ be a type with u finite and functions f,g,f₁,f₂,g' with h_distrib: ∀ a b c, f (g a b) c = g' (f₁ a c) (f₂ b c). Then image₂ f (image₂ g s t) u ⊆ image₂ g' (image₂ f₁ s u) (image₂ f₂ t u).
Русский
Пусть Γ — множество, u — подмножество; если выполняется распределение g по f в виде h_distrib, то image₂ f (image₂ g s t) u ⊆ image₂ g' (image₂ f₁ s u) (image₂ f₂ t u).
LaTeX
$$$\\forall s,t,u:\\ Finset\\,\\alpha,\\beta,\\gamma,\\delta,\\n \\qquad (\\forall a,b,c, f (g a b) c = g' (f₁ a c) (f₂ b c)) \\Rightarrow image_2 f (image_2 g s t) u \\subseteq image_2 g' (image_2 f₁ s u) (image_2 f₂ t u) $$$
Lean4
/-- The other direction does not hold because of the `u`-`u` cross terms on the RHS. -/
theorem image₂_distrib_subset_right {γ : Type*} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ} {f₁ : α → γ → α'}
{f₂ : β → γ → β'} {g' : α' → β' → ε} (h_distrib : ∀ a b c, f (g a b) c = g' (f₁ a c) (f₂ b c)) :
image₂ f (image₂ g s t) u ⊆ image₂ g' (image₂ f₁ s u) (image₂ f₂ t u) :=
coe_subset.1 <| by
push_cast
exact Set.image2_distrib_subset_right h_distrib
