invFun_eq_of_injective_of_rightInverse

English

If f is injective and g is a right inverse of f, then invFun f = g.

Русский

Если f инъективна и g является правой обратной к f, тогда invFun f = g.

LaTeX

$$$ \text{Injective}(f) \rightarrow \text{RightInverse}(g,f) \rightarrow \mathrm{invFun}(f) = g $$$

Lean4

theorem invFun_eq_of_injective_of_rightInverse {g : β → α} (hf : Injective f) (hg : RightInverse g f) : invFun f = g :=
  funext fun b ↦
    hf
      (by
        rw [hg b]
        exact invFun_eq ⟨g b, hg b⟩)

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