apply_symm_apply — Mathlib

English

For an algebra equivalence e, the inverse map composed with e is the identity on the target; i.e. e.symm applied after e yields the identity on A2.

Русский

Для эквивалентности e обратная карта после применения e является тождественной на целевом пространстве.

LaTeX

$$$\forall x, e^{-1}(e(x)) = x$$$

Lean4

@[simp]
theorem apply_symm_apply (e : A₁ ≃ₐ[R] A₂) : ∀ x, e (e.symm x) = x :=
  e.toEquiv.apply_symm_apply

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