invFun_restrict — Mathlib

English

The restriction of the inverse function invFun f to the range of f coincides with invOfMemRange.

Русский

Ограничение обратной функции invFun f до образа f совпадает с invOfMemRange.

LaTeX

$$$ (\\mathrm{Set.range}(f))\\restriction (\\mathrm{invFun}(f)) = \\mathrm{invOfMemRange} $$$

Lean4

theorem invFun_restrict [Nonempty α] : (Set.range f).restrict (invFun f) = hf.invOfMemRange :=
  by
  ext ⟨b, h⟩
  apply hf
  simp [hf.left_inv_of_invOfMemRange, @invFun_eq _ _ _ f b (Set.mem_range.mp h)]

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