rightInvOn_invFunOn — Mathlib

English

If f is surjective on s onto t, then invFunOn f s is a right inverse for f on t.

Русский

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

LaTeX

$$$$\\operatorname{SurjOn}(f, s, t) \\Rightarrow \\operatorname{RightInvOn}(\\operatorname{invFunOn} f s, f, t).$$$$

Lean4

theorem rightInvOn_invFunOn [Nonempty α] (h : SurjOn f s t) : RightInvOn (invFunOn f s) f t := fun _y hy =>
  invFunOn_eq <| h hy

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