span_univ

Mathlib.Algebra.Lie.Subalgebra

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

English

The Lie span of the universal set is the top subalgebra: lieSpan_R L(Set.univ) = ⊤.

Русский

Lie-порождение всего множества равно верхней подпалгебре: lieSpan_R L(Set.univ) = ⊤.

LaTeX

$$$\\operatorname{lieSpan}_R L(\\mathrm{Set.univ}) = \\top$$$

Lean4

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

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

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

Разделы

Аффилиация

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