English
Let s be a finite set and suppose there are functions f, g, f', g' with h_comm: ∀ a, f(g(a)) = g'(f'(a)). Then applying image to g and then f equals applying image to f' and then g' on s: (image g s).image f = (image f' s).image g'.
Русский
Пусть s — конечное множество и существуют функции f, g, f', g' such that h_comm: ∀ a, f(g(a)) = g'(f'(a)). Тогда образ по g, затем по f равен образу по f', затем по g' на s: (image g s).image f = (image f' s).image g'.
LaTeX
$$$\Bigl(\mathrm{image}\ g\ s\Bigr).\mathrm{image}\ f = \Bigl(\mathrm{image}\ f'\ s\Bigr).\mathrm{image}\ g' \quad\text{where } \forall a, f(g(a)) = g'(f'(a))$$$
Lean4
theorem image_comm {β'} [DecidableEq β'] [DecidableEq γ] {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ}
(h_comm : ∀ a, f (g a) = g' (f' a)) : (s.image g).image f = (s.image f').image g' := by
simp_rw [image_image, comp_def, h_comm]
