apply_symm_apply — Mathlib

English

For any ordered monoid isomorphism e and any element y, applying e after its inverse yields y: e(e.symm(y)) = y.

Русский

Для любого упорядоченного изоморфизма e и элемента y применение e после его обратного дает y: e(e.symm(y)) = y.

LaTeX

$$$e\\bigl(e^{-1}(y)\\bigr) = y$$$

Lean4

/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`. -/
@[to_additive (attr := simp) /-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`. -/
    ]
theorem apply_symm_apply (e : α ≃*o β) (y : β) : e (e.symm y) = y :=
  e.toEquiv.apply_symm_apply y

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