English
If there exists a in s with f a = b, then invFunOn f s b lies in s and f(invFunOn f s b) = b.
Русский
Если существует a∈s такое, что f a = b, то invFunOn f s b находится в s и выполняется равенство f(invFunOn f s b) = b.
LaTeX
$$$$\\big(\\exists a \\in s, f a = b\\big) \\Rightarrow \\operatorname{invFunOn} f s b \\in s \\land f(\\operatorname{invFunOn} f s b) = b.$$$$
Lean4
theorem invFunOn_mem (h : ∃ a ∈ s, f a = b) : invFunOn f s b ∈ s :=
(invFunOn_pos h).left