eqOn_lieSpan — Mathlib

English

If two LieDerivations agree on a set s, they agree on the Lie span of s as well.

Русский

Если два LieDerivation совпадают на наборе s, они совпадают на Lie-образе s.

LaTeX

$$$\text{If } \text{EqOn } D_1 D_2 s, \text{ then } \text{EqOn } D_1 D_2(\operatorname{lieSpan} R L s)$$$

Lean4

/-- Two Lie derivations equal on a set are equal on its Lie span. -/
theorem eqOn_lieSpan {s : Set L} (h : Set.EqOn D1 D2 s) : Set.EqOn D1 D2 (LieSubalgebra.lieSpan R L s) :=
  by
  intro _ hx
  induction hx using LieSubalgebra.lieSpan_induction with
  | mem x hx => exact h hx
  | zero => simp
  | add x y _ _ hx hy => simp [hx, hy]
  | smul t x _ hx => simp [hx]
  | lie x y _ _ hx hy => simp [hx, hy]

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