injOn_preimage — Mathlib

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)

Похожие утверждения