lieBracketWithin_const_smul_left — Mathlib

English

For a scalar c, lieBracket 𝕜 (c • V) W x = c • lieBracket 𝕜 V W x when V is differentiable at x.

Русский

При скаляре c скобка Ли слева от V масштабируется на c: [cV,W](x) = c[V,W](x), если V дифференцируема в x.

LaTeX

$$$\operatorname{lieBracket} 𝕜 (c \cdot V) W x = c \cdot \operatorname{lieBracket} 𝕜 V W x$$$

Lean4

theorem lieBracketWithin_const_smul_left {c : 𝕜} (hV : DifferentiableWithinAt 𝕜 V s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
    lieBracketWithin 𝕜 (c • V) W s x = c • lieBracketWithin 𝕜 V W s x := by
  simp [lieBracketWithin, smul_sub, fderivWithin_const_smul hs hV]

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