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