English
Let h be a semiconjugacy f ∘ fa = fb ∘ f. If fa is injective on a set s and f is injective on fa '' s, then fb is injective on f '' s.
Русский
Пусть h является полусопряжением: f ∘ fa = fb ∘ f. Если fa инъективна на s и f инъективна на fa(s), то fb инъективна на f(s).
LaTeX
$$$ (f \\circ fa = fb \\circ f) \\Rightarrow (\\operatorname{InjOn} fa\ \(s)) \\Rightarrow (\\operatorname{InjOn} f (fa'' s)) \\Rightarrow \\operatorname{InjOn} fb (f'' s). $$$
Lean4
theorem injOn_image (h : Semiconj f fa fb) (ha : InjOn fa s) (hf : InjOn f (fa '' s)) : InjOn fb (f '' s) :=
by
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ H
simp only [← h.eq] at H
exact congr_arg f (ha hx hy <| hf (mem_image_of_mem fa hx) (mem_image_of_mem fa hy) H)
