English
Let h be a semiconjugacy f fa fb. If fa is bijective on s to t, and f is injective on t, then fb is bijective on image f s to image f t.
Русский
Пусть h является полусопряжением f fa fb. Если fa биекция между s и t, и f инъективна на t, тогда fb биекция между f''s и f''t.
LaTeX
$$$ (f \\circ fa = fb \\circ f) \\Rightarrow (\\operatorname{BijOn} fa\ s\\ t) \\Rightarrow (\\operatorname{InjOn} f\\ t) \\Rightarrow \\operatorname{BijOn} fb (f'' s) (f'' t). $$$
Lean4
theorem bijOn_image (h : Semiconj f fa fb) (ha : BijOn fa s t) (hf : InjOn f t) : BijOn fb (f '' s) (f '' t) :=
⟨h.mapsTo_image ha.mapsTo, h.injOn_image ha.injOn (ha.image_eq.symm ▸ hf), h.surjOn_image ha.surjOn⟩
