toSubmodule_mk — Mathlib

English

If you form a LieSubalgebra from a Submodule p with a compatible Lie_mem' structure h, then the underlying Submodule is exactly p.

Русский

Пусть p — подподпространство, а lie_mem' обеспечивает совместимость. Тогда носитель подалгебры совпадает с p.

LaTeX

$$$$\forall (p : \text{Submodule } R L) (h),\big(({ p \text{ with lie_mem' := h }} : \text{LieSubalgebra } R L) : \text{Submodule } R L\big) = p.$$$$

Lean4

theorem toSubmodule_mk (p : Submodule R L) (h) : (({ p with lie_mem' := h } : LieSubalgebra R L) : Submodule R L) = p :=
  rfl

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