bijOn_range — Mathlib

English

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

Русский

Пусть h является полусопряжением f fa fb. Если fa биекция и f инъективна, то fb биекция на range(f).

LaTeX

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

Lean4

theorem bijOn_range (h : Semiconj f fa fb) (ha : Bijective fa) (hf : Injective f) : BijOn fb (range f) (range f) :=
  by
  rw [← image_univ]
  exact h.bijOn_image (bijective_iff_bijOn_univ.1 ha) hf.injOn

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