leftInvOn_invFunOn — Mathlib

English

If f is injective on s and there exists a left inverse of f on t, then invFunOn f s serves as a left inverse on s.

Русский

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

LaTeX

$$$$\\text{[Nonempty }\\alpha]\\; \\text{theorem: } \\text{LeftInvOn}(\\operatorname{invFunOn} f s, f, s).$$$$

Lean4

theorem leftInvOn_invFunOn [Nonempty α] (h : InjOn f s) : LeftInvOn (invFunOn f s) f s := fun _a ha =>
  h (invFunOn_apply_mem ha) ha (invFunOn_apply_eq ha)

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