invFunOn_image — Mathlib

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

Похожие утверждения