English
Let f, ga, gb be maps with a semiconjugacy h: f ∘ ga = gb ∘ f. Then the induced maps on sets satisfy a semiconjugacy: image f semiconjugate to image ga and image gb, i.e. for all S, f '' (ga '' S) = gb '' (f '' S).
Русский
Пусть f, ga, gb — отображения и существует полусогласование h: f ∘ ga = gb ∘ f. Тогда переход к множествам сохраняет полусогласование: образы под f и ga образуют полусогласование по отношению к gb и образу f.
LaTeX
$$$ \\forall S,\\ f '' (ga '' S) = gb '' (f '' S) \\quad \\text{when } \\forall x,\\ f(ga(x)) = gb(f(x)). $$$
Lean4
theorem _root_.Function.Semiconj.set_image {f : α → β} {ga : α → α} {gb : β → β} (h : Function.Semiconj f ga gb) :
Function.Semiconj (image f) (image ga) (image gb) := fun _ => image_comm h
