lieSpan_le — Mathlib

English

For any Lie-submodule N, lieSpan(s) ≤ N if and only if s ⊆ N. In words, lieSpan is the smallest Lie-submodule containing s.

Русский

Для любого подмодуля N верно: lieSpan(s) ≤ N тогда и только тогда, когда s ⊆ N. Так lieSpan является наименьшим Лие-подмодулем, содержащим s.

LaTeX

$$\\operatorname{lieSpan}_{R,L}(s) \\le N \\;\\iff\\; s \\subseteq N$$

Lean4

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

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