apply_symm_apply — Mathlib

English

For any equivalence e and x in β, e (e.symm x) = x; i.e., applying e after its inverse recovers the original element.

Русский

Для любой эквивалки e и x из β, e(e.symm x)=x; то есть применение e после обратного отображения возвращает исходный элемент.

LaTeX

$$$e (e^{-1}(x)) = x.$$$

Lean4

@[simp, grind =]
theorem apply_symm_apply (e : α ≃ β) (x : β) : e (e.symm x) = x :=
  e.right_inv x

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