English
Let h be a semiconjugacy f fa fb. If fb is injective on s and f is injective on f⁻¹'(s), then fa is injective on f⁻¹'(s).
Русский
Пусть h является полусопряжением f fa fb. Если fb инъективна на s и f инъективна на f⁻¹'(s), то fa инъективна на f⁻¹'(s).
LaTeX
$$$ (f \\circ fa = fb \\circ f) \\Rightarrow (\\operatorname{InjOn} fb s) \\Rightarrow (\\operatorname{InjOn} f (f^{-1}' s)) \\Rightarrow \\operatorname{InjOn} fa (f^{-1}' s). $$$
Lean4
theorem injOn_preimage (h : Semiconj f fa fb) {s : Set β} (hb : InjOn fb s) (hf : InjOn f (f ⁻¹' s)) :
InjOn fa (f ⁻¹' s) := by
intro x hx y hy H
have := congr_arg f H
rw [h.eq, h.eq] at this
exact hf hx hy (hb hx hy this)