English
If s ⊆ invFunOn f s '' (f '' s), then invFunOn f s is a left inverse on s.
Русский
Если s является подмножеством образа обратной функции на s то есть содержит все свои изображения под f, то invFunOn f s является левой обратной на s.
LaTeX
$$$$\\text{[Nonempty }\\alpha] \\; s \\subseteq (\\operatorname{invFunOn} f s) '' (f '' s) \\Rightarrow \\operatorname{LeftInvOn}(\\operatorname{invFunOn} f s, f, s).$$$$
Lean4
theorem _root_.Function.leftInvOn_invFunOn_of_subset_image_image [Nonempty α] (h : s ⊆ (invFunOn f s) '' (f '' s)) :
LeftInvOn (invFunOn f s) f s := fun x hx ↦
by
obtain ⟨-, ⟨x, hx', rfl⟩, rfl⟩ := h hx
rw [invFunOn_apply_eq (f := f) hx']