English
If f is injective on s2 and s1 ⊆ s2, then invFunOn f s2 '' (f '' s1) = s1.
Русский
Если f инъективна на s2 и s1 ⊆ s2, то invFunOn f s2 примененная к изображению f''s1 дает s1.
LaTeX
$$$$\\operatorname{InjOn}(f, s_2) \\land s_1 \\subseteq s_2 \\Rightarrow \\operatorname{invFunOn} f s_2 '' (f '' s_1) = s_1.$$$$
Lean4
theorem invFunOn_image [Nonempty α] (h : InjOn f s₂) (ht : s₁ ⊆ s₂) : invFunOn f s₂ '' (f '' s₁) = s₁ :=
h.leftInvOn_invFunOn.image_image' ht