bijOn_subset — Mathlib

English

If f maps s bijectively onto t, then f restricted to invFunOn f s '' t is a bijection onto t.

Русский

Если f отображает s биективно на t, то ограничение f на invFunOn f s '' t задаёт биективное отображение на t.

LaTeX

$$$[\\text{Nonempty }\\alpha] (h : BijOn f s t) \\Rightarrow BijOn f (invFunOn f s '' t) t$$$

Lean4

theorem bijOn_subset [Nonempty α] (h : SurjOn f s t) : BijOn f (invFunOn f s '' t) t :=
  by
  refine h.invOn_invFunOn.bijOn ?_ (mapsTo_image _ _)
  rintro _ ⟨y, hy, rfl⟩
  rwa [h.rightInvOn_invFunOn hy]

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