left_inv' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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