English
If f is surjective on s to t, then the image under f of the inverse image of a subset r of t equals r.
Русский
Если f сюръективна с s на t, то образ f от invFunOn s '' r равен r для любого r ⊆ t.
LaTeX
$$$[\\text{Nonempty }\\alpha] \\ SurjOn f s t \\rightarrow f '' (f.invFunOn s '' r) = r$$$
Lean4
/-- This lemma is a special case of `rightInvOn_invFunOn.image_image`; it may make more sense
to use the other lemma directly in an application. -/
theorem image_invFunOn_image [Nonempty α] (hf : SurjOn f s t) : f '' (f.invFunOn s '' t) = t :=
hf.rightInvOn_invFunOn.image_image