leftInvOn_invFunOn_of_subset_image_image

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']

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