mem_lieSpan — Mathlib

English

Let s be a subset of a Lie algebra L over R. An element x belongs to lieSpan_R L s if and only if x belongs to every LieSubalgebra of L that contains s.

Русский

Пусть s ⊆ L. Элемент x принадлежит lieSpan_R L s тогда и только тогда, когда он принадлежит каждой подпалгебре Ли L, содержащей s.

LaTeX

$$$x\\in \\operatorname{lieSpan}_R L(s) \\;\\iff\\; \\forall K:\\\\text{LieSubalgebra}_R L,\\ s\\subseteq K\\ \\to\\ x\\in K$$$

Lean4

theorem mem_lieSpan {x : L} : x ∈ lieSpan R L s ↔ ∀ K : LieSubalgebra R L, s ⊆ K → x ∈ K :=
  by
  rw [← SetLike.mem_coe, lieSpan, coe_sInf]
  exact Set.mem_iInter₂

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