English
If a semiconjugacy f ∘ ga = gb ∘ f holds between functions on α, then the induced image-map is a semiconjugacy between image ga and image gb via image f.
Русский
Если существует полумультипараллелизм f ∘ ga = gb ∘ f между функциями на α, то индуцированное отображение образа устанавливает полумультипараллелизм между image ga и image gb через image f.
LaTeX
$$$\bigl(\forall x,\; f(ga(x)) = gb(f(x))\bigr) \Rightarrow \forall s,\; \mathrm{image}\ f\, (\mathrm{image}\ ga\ s) = \mathrm{image}\ gb\ (\mathrm{image}\ f\ s)$$$
Lean4
theorem _root_.Function.Semiconj.finset_image [DecidableEq α] {f : α → β} {ga : α → α} {gb : β → β}
(h : Function.Semiconj f ga gb) : Function.Semiconj (image f) (image ga) (image gb) := fun _ => image_comm h
