lieBracket — Mathlib

English

For differentiable f and V, the Lie bracket of f•V with W satisfies a left 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}_{\mathbb{K}}(fV, W)(x) = - (fderiv_{\mathbb{K}} f)(W x) \cdot V x + f(x) \operatorname{lieBracket}_{\mathbb{K}}(V, W)(x)$$$

Lean4

/-- The Lie bracket `[V, W] (x)` of two vector fields at a point, defined as
`DW(x) (V x) - DV(x) (W x)`. -/
def lieBracket (V W : E → E) (x : E) : E :=
  fderiv 𝕜 W x (V x) - fderiv 𝕜 V x (W x)

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