ext_of_lieSpan_eq_top — Mathlib

English

If the Lie span of a set s is the entire Lie algebra, then equalities on s extend to the whole algebra for LieDerivation.

Русский

Если Lie-образование LieSpan(s) равно всей алгебре, равенства на s распространяются на всю алгебру.

LaTeX

$$$\operatorname{lieSpan}_R L s = \top \Rightarrow (\forall a\in s, D_1 a = D_2 a) \Rightarrow D_1 = D_2$$$

Lean4

/-- If the Lie span of a set is the whole Lie algebra, then two Lie derivations equal on this set
are equal on the whole Lie algebra. -/
theorem ext_of_lieSpan_eq_top (s : Set L) (hs : LieSubalgebra.lieSpan R L s = ⊤) (h : Set.EqOn D1 D2 s) : D1 = D2 :=
  ext fun _ => eqOn_lieSpan h <| hs.symm ▸ trivial

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