rightInverse_symm — Mathlib

English

For e ∈ A ≃⋆* B, e is a left inverse of e.symm and e.symm is a right inverse of e; equivalently, for all b ∈ B, e (e.symm b) = b.

Русский

Для e ∈ A ≃⋆* B e.symm — левый обратный к e, а e — правый обратный к e.symm; то есть для всех b ∈ B выполняется e(e.symm b) = b.

LaTeX

$$$\\forall b,\\ e(e.symm(b)) = b$$$

Lean4

theorem rightInverse_symm (e : A ≃⋆* B) : Function.RightInverse e.symm e :=
  e.right_inv

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