apply_symm_apply — Mathlib

English

For any multiplicative equivalence e: M ≃* N and any y ∈ N, e(e.symm(y)) = y; the symmetrized map is a two-sided inverse.

Русский

Для любого изоморфизма e: M ≃* N и любого y ∈ N верно e(e.symm(y)) = y; симметричная карта является двухсторонним обратным.

LaTeX

$$$e(e^{-1}(y)) = 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 : M ≃* N) (y : N) : e (e.symm y) = y :=
  e.toEquiv.apply_symm_apply y

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