injOn_range — Mathlib

English

Let h be a semiconjugacy f fa fb. If fa is injective and f is injective on range fa, then fb is injective on range f.

Русский

Пусть h является полусопряжением f fa fb. Если fa инъективна и f инъективна на диапазоне fa, то fb инъективна на диапазоне f.

LaTeX

$$$ (f \\circ fa = fb \\circ f) \\Rightarrow (\\operatorname{Injective} fa) \\Rightarrow (\\operatorname{InjOn} f (\\operatorname{range} fa)) \\Rightarrow \\operatorname{InjOn} fb (\\operatorname{range} f). $$$

Lean4

theorem injOn_range (h : Semiconj f fa fb) (ha : Injective fa) (hf : InjOn f (range fa)) : InjOn fb (range f) :=
  by
  rw [← image_univ] at *
  exact h.injOn_image ha.injOn hf

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