lieSpan_le

Mathlib.Algebra.Lie.Subalgebra

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

← MathLib Explorer

English

If s ⊆ t, then lieSpan_R L s ≤ lieSpan_R L t.

Русский

Если s ⊆ t, тогда lieSpan_R L s ≤ lieSpan_R L t.

LaTeX

$$$s \\subseteq t \\Rightarrow \\operatorname{lieSpan}_R L(s) \\le \\operatorname{lieSpan}_R L(t)$$$

Lean4

theorem lieSpan_le {K} : lieSpan R L s ≤ K ↔ s ⊆ K := by
  constructor
  · exact Set.Subset.trans subset_lieSpan
  · intro hs m hm
    rw [mem_lieSpan] at hm
    exact hm _ hs

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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