lieBracketWithin_eq — Mathlib

English

The Lie bracket is additive in its first argument: lieBracket(V+V1, W) = lieBracket(V, W) + lieBracket(V1, W).

Русский

Скобка Ли аддитивна по первому аргументу: [V+V1, W] = [V, W] + [V1, W].

LaTeX

$$$\operatorname{lieBracket}(V+V_1, W)(x) = \operatorname{lieBracket}(V, W)(x) + \operatorname{lieBracket}(V_1, W)(x)$$$

Lean4

theorem lieBracketWithin_eq :
    lieBracketWithin 𝕜 V W s = fun x ↦ fderivWithin 𝕜 W s x (V x) - fderivWithin 𝕜 V s x (W x) :=
  rfl

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