toEquiv_injective — Mathlib

English

The map sending a Lie module equivalence to its underlying Equiv is injective.

Русский

Отображение, отправляющее эквивалентность Ли-модуля в соответствующую действительную эквивалентность, инъективно.

LaTeX

$$$\\forall e_1,e_2,\\toEquiv(e_1) = \\toEquiv(e_2) \\Rightarrow e_1 = e_2$$$

Lean4

theorem toEquiv_injective : Function.Injective (toEquiv : (M ≃ₗ⁅R,L⁆ N) → M ≃ N) :=
  by
  rintro ⟨⟨⟨⟨f, -⟩, -⟩, -⟩, f_inv⟩ ⟨⟨⟨⟨g, -⟩, -⟩, -⟩, g_inv⟩
  simp

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