apply_inv_apply — Mathlib

English

For any EquivLike structure e and any b, applying e to inv e b yields b.

Русский

Для любой структуры EquivLike применение e к inv e b даёт b.

LaTeX

$$$e(\text{inv}(e,b)) = b$$$

Lean4

/-- This lemma is only supposed to be used in the generic context, when working with instances
of classes extending `EquivLike`.
For concrete isomorphism types such as `Equiv`, you should use `Equiv.apply_symm_apply`
or its equivalent.

TODO: define a generic form of `Equiv.symm`. -/
@[simp]
theorem apply_inv_apply (e : E) (b : β) : e (inv e b) = b :=
  right_inv _ _

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