invFunOn_injOn_image — Mathlib

English

For any nonempty α, invFunOn f s is injective on the image f''s.

Русский

Если f инъективна на s, то invFunOn f s инъективна на образе s.

LaTeX

$$$$\\forall [Nonempty\\ α], \\operatorname{InjOn}(\\operatorname{invFunOn} f s, f'' s).$$$$

Lean4

theorem _root_.Function.invFunOn_injOn_image [Nonempty α] (f : α → β) (s : Set α) : Set.InjOn (invFunOn f s) (f '' s) :=
  by
  rintro _ ⟨x, hx, rfl⟩ _ ⟨x', hx', rfl⟩ he
  rw [← invFunOn_apply_eq (f := f) hx, he, invFunOn_apply_eq (f := f) hx']

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