symm_apply_apply — Mathlib

English

The symmetric application followed by the original application yields the identity on the domain; i.e. e.symm (e x) = x for all x.

Русский

Симметричное применение затем исходное применение дает тождество на области определения.

LaTeX

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

Lean4

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

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