injOn_iff_invFunOn_image_image_eq_self

English

If f surjects onto t from s, then invFunOn f s is an inverse relation on s with f.

Русский

Для любого непустого α, f и s дают равенство изображений invFunOn и f на s, когда s является подмножеством образа invFunOn f s и образа f s.

LaTeX

$$$$\\operatorname{Set.SurjOn}(f, s, t) \\Rightarrow \\operatorname{InvOn}(\\operatorname{Function.invFunOn} f s, f, s, t).$$$$

Lean4

theorem injOn_iff_invFunOn_image_image_eq_self [Nonempty α] : InjOn f s ↔ (invFunOn f s) '' (f '' s) = s :=
  ⟨fun h ↦ h.invFunOn_image Subset.rfl, fun h ↦ (Function.leftInvOn_invFunOn_of_subset_image_image h.symm.subset).injOn⟩

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