symm_apply_apply — Mathlib

English

For any coalgebra equivalence e: A ≃ₗc[R] B and any element x ∈ A, applying e and then its inverse returns x: e^{-1}(e(x)) = x.

Русский

Для любой коалг-близости e: A ≃ₗc[R] B и любого элемента x ∈ A применение e, затем его обратного отображения возвращает x: e^{-1}(e(x)) = x.

LaTeX

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

Lean4

@[simp]
theorem symm_apply_apply (e : A ≃ₗc[R] B) (x) : e.symm (e x) = x :=
  LinearEquiv.symm_apply_apply (e : A ≃ₗ[R] B) x

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