symm_apply_apply — Mathlib

English

For any x ∈ M, e.symm(e(x)) = x; the forward map recovers the input after applying the inverse.

Русский

Для любого x ∈ M выполняется e.symm(e(x)) = x; обратная карта восстанавливает вход.

LaTeX

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

Lean4

/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`. -/
@[to_additive (attr := simp) /-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`. -/
    ]
theorem symm_apply_apply (e : M ≃* N) (x : M) : e.symm (e x) = x :=
  e.toEquiv.symm_apply_apply x

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