English
Let s ⊆ α and t ⊆ β be finite sets. If f: α' → β → γ, g: α → α', f': α → β → δ, and g': δ → γ satisfy f(g(a), b) = g'(f'(a,b)) for all a,b, then applying image₂ with g on s and t is the same as applying image₂ with f' on s and t and then composing with g'. In symbols, image₂ f (image g s) t = (image₂ f' s t).image g'.
Русский
Пусть s ⊆ α и t ⊆ β — конечные множества. Пусть f: α' → β → γ, g: α → α', f': α → β → δ, g': δ → γ, и выполнено условие h_left_comm: ∀ a,b, f (g a) b = g' (f' a b). Тогда применение image₂ по g слева к s и t эквивалентно применению image₂ к s,t через f', после чего полученное множество приводится к γ функцией g'. То есть image₂ f (image g s) t = (image₂ f' s t).image g'.
LaTeX
$$$\\forall s:\\ Finset\\,\\alpha\\,\\forall t:\\ Finset\\,\\beta\\,\\Big(\\forall a,b, f (g a) b = g' (f' a b) \\Big) \\Rightarrow \\ Fer image_2 f (image g\, s) t = (image_2 f' s t).image g' $$$
Lean4
/-- Symmetric statement to `Finset.image_image₂_distrib_left`. -/
theorem image₂_image_left_comm {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ}
(h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) : image₂ f (s.image g) t = (image₂ f' s t).image g' :=
(image_image₂_distrib_left fun a b => (h_left_comm a b).symm).symm
