inv_apply_apply — Mathlib

English

For any EquivLike structure e and any a, applying the inverse of e to e(a) returns a.

Русский

Для любой структуры EquivLike и любого элемента a применение обратного отображения к e(a) возвращает a.

LaTeX

$$$\text{inv}(e)(e(a)) = a$$$

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.symm_apply_apply`
or its equivalent.

TODO: define a generic form of `Equiv.symm`. -/
@[simp]
theorem inv_apply_apply (e : E) (a : α) : inv e (e a) = a :=
  left_inv _ _

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