invOn_invFunOn — Mathlib

English

If f is surjective on s to t, then invFunOn f s provides an inverse-on relation between invFunOn f s on its image and f on t.

Русский

Если f сюръективна, то invFunOn f s образует взаимную обратимость через образ функции.

LaTeX

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

Lean4

theorem invOn_invFunOn [Nonempty α] (h : SurjOn f s t) : InvOn (invFunOn f s) f (invFunOn f s '' t) t :=
  by
  refine ⟨?_, h.rightInvOn_invFunOn⟩
  rintro _ ⟨y, hy, rfl⟩
  rw [h.rightInvOn_invFunOn hy]

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