coe_injective — Mathlib

English

The map sending a Lie subalgebra to its underlying set is injective.

Русский

Отображение подалгебры в соответствующее множество инъективно.

LaTeX

$$$$\forall {R} {L} [\text{CommRing } R] [\text{LieRing } L] [\text{LieAlgebra } R L], \text{Function.Injective} (\uparrow) : \text{LieSubalgebra } R L \to \text{Set } L.$$$$

Lean4

theorem coe_injective : Function.Injective ((↑) : LieSubalgebra R L → Set L) :=
  SetLike.coe_injective

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