English
Let V, W, W1 be vector fields on a normed space E over a nontrivially normed field 𝕜. If W and W1 are differentiable at a point x, then the Lie bracket is additive in the second argument at x: [V, W + W1](x) = [V, W](x) + [V, W1](x).
Русский
Пусть V, W, W1 — векторные поля на нормированном пространстве E над ненулевым нормированным полем 𝕜. Если W и W1 дифференцируемы в точке x, то скобка Ли относительно V и W+W1 в точке x распадается на сумму скобок Ли по V и W и V и W1: [V, W+W1](x) = [V, W](x) + [V, W1](x).
LaTeX
$$$[V, W+W_{1}]_{\\\\mathfrak{k}}(x) = [V, W]_{\\\\mathfrak{k}}(x) + [V, W_{1}]_{\\\\mathfrak{k}}(x)$$$
Lean4
theorem lieBracket_add_right (hW : DifferentiableAt 𝕜 W x) (hW₁ : DifferentiableAt 𝕜 W₁ x) :
lieBracket 𝕜 V (W + W₁) x = lieBracket 𝕜 V W x + lieBracket 𝕜 V W₁ x :=
by
simp only [lieBracket, Pi.add_apply, map_add]
rw [fderiv_add hW hW₁, ContinuousLinearMap.add_apply]
abel
