right_inv' — Mathlib

English

For any e: α ≃ β, the inverse e^{-1} is a right inverse of e, i.e., e ∘ e^{-1} = id_β.

Русский

Для любой e: α ≃ β обратное отображение e^{-1} является правым обратным к e: e ∘ e^{-1} = id_β.

LaTeX

$$$e \circ e^{-1} = \mathrm{id}_{\beta}$$$

Lean4

/-- Restatement of `Equiv.right_inv` in terms of `Function.RightInverse`. -/
theorem right_inv' (e : α ≃ β) : Function.RightInverse e.symm e :=
  e.right_inv

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