English
Let s be a subset of α and suppose f, f', g, g' are maps with f ◦ g = g' ◦ f'. Then the two-step image of s under g and then f equals the two-step image of s under f' and then g', i.e. (s image g) image f = (s image f') image g'.
Русский
Пусть s ⊆ α и пусть существуют отображения f, f', g, g', такие что f ∘ g = g' ∘ f'. Тогда образ двойной последовательности применения образов к s совпадает: (s образ g) образ f = (s образ f') образ g'.
LaTeX
$$$ (s \\text{ image } g) \\text{ image } f = (s \\text{ image } f') \\text{ image } g' \\quad \\text{provided } \\forall a,\\ f(g(a)) = g'(f'(a)). $$$
Lean4
theorem image_comm {β'} {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ} (h_comm : ∀ a, f (g a) = g' (f' a)) :
(s.image g).image f = (s.image f').image g' := by grind
