span_univ

Mathlib.Algebra.Lie.Submodule

URI: https://scilib.ai/kg/mathlib#LieSubmodule.span_univ

English

The lie-span of the whole space is the top submodule: lieSpan R L Set.univ = ⊤.

Русский

lie-span всего пространства равен верхнему подмодулю: lieSpan R L Set.univ = ⊤.

LaTeX

$$lieSpan_{R,L}(\\mathrm{Set.univ}) = \\top$$

Lean4

@[simp]
theorem span_univ : lieSpan R L (Set.univ : Set M) = ⊤ :=
  eq_top_iff.2 <| SetLike.le_def.2 <| subset_lieSpan

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru