apply_eq_iff_eq_symm_apply — Mathlib

English

The map toEquiv from LieModuleEquiv to Equiv is injective.

Русский

Отображение toEquiv из эквивалентности Ли-модуля в обычную эквивалентность инъективно.

LaTeX

$$$\\text{toEquiv is injective: } \\forall e_1,e_2,\\toEquiv(e_1)=\\toEquiv(e_2) \\Rightarrow e_1=e_2$$$

Lean4

theorem apply_eq_iff_eq_symm_apply {m : M} {n : N} (e : M ≃ₗ⁅R,L⁆ N) : e m = n ↔ m = e.symm n :=
  (e : M ≃ N).apply_eq_iff_eq_symm_apply

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