lieBracketWithin — Mathlib

English

If W is differentiable at x, then [V, cW] = c [V, W] for any scalar c ∈ 𝕜.

Русский

Если W дифференцируема в точке x, то [V, cW] = c [V, W] для любого скаляра c ∈ 𝕜.

LaTeX

$$$\operatorname{lieBracket}(V, cW)(x) = c \operatorname{lieBracket}(V, W)(x)$$$

Lean4

/-- The Lie bracket `[V, W] (x)` of two vector fields within a set at a point, defined as
`DW(x) (V x) - DV(x) (W x)` where the derivatives are taken inside `s`. -/
def lieBracketWithin (V W : E → E) (s : Set E) (x : E) : E :=
  fderivWithin 𝕜 W s x (V x) - fderivWithin 𝕜 V s x (W x)

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