coe_injective — Mathlib

English

The underlying set map from LieSubmodule R L M to Set M is injective; i.e., if two LieSubmodules have the same carrier set, they are equal.

Русский

Пусть два LieSubmoduleR L M имеют одинаковое множество элементов; тогда они равны.

LaTeX

$$$ \forall N,N' : LieSubmodule\ R\ L\ M,\ (N : Set M) = (N' : Set M) \Rightarrow N = N' $$$

Lean4

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

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