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]