lieBracket_eq — Mathlib

English

For differentiable f and V, the Lie bracket with left scaling obeys a product rule: [f•V, W] = - (df W) • V + f • [V, W].

Русский

Для дифференцируемого f и V выполняется правило произведения слева: [f•V, W] = - (df W) • V + f • [V, W].

LaTeX

$$$\operatorname{lieBracket}(fV, W)(x) = - (fderiv f)(W x) \cdot V x + f(x) \operatorname{lieBracket}(V, W)(x)$$$

Lean4

theorem lieBracket_eq : lieBracket 𝕜 V W = fun x ↦ fderiv 𝕜 W x (V x) - fderiv 𝕜 V x (W x) :=
  rfl

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