lieBracket_const_smul_left — Mathlib

English

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

Русский

Для скаляра 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 lieBracket_const_smul_left {c : 𝕜} (hV : DifferentiableAt 𝕜 V x) :
    lieBracket 𝕜 (c • V) W x = c • lieBracket 𝕜 V W x :=
  by
  simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ] at hV ⊢
  exact lieBracketWithin_const_smul_left hV uniqueDiffWithinAt_univ

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