lieBracket_const_smul_right — Mathlib

English

If f: E → 𝕜 is differentiable at x and W is differentiable at x, then [V, f·W] = (Df f)(x)(Vx)·W(x) + f(x)·[V, W](x).

Русский

Если f: E → 𝕜 дифференцируема в x и W дифференцируема в x, то [V, f·W] = (Df f)(x)(Vx)·W(x) + f(x)·[V, W](x).

LaTeX

$$$\mathrm{lieBracketWithin}(V, f\cdot W) = (\mathrm{fderivWithin}\mathbb{K}f\, x)(Vx)\cdot Wx + f(x)\cdot \mathrm{lieBracketWithin}(V, W, s, x)$$$

Lean4

theorem lieBracket_const_smul_right {c : 𝕜} (hW : DifferentiableAt 𝕜 W x) :
    lieBracket 𝕜 V (c • W) x = c • lieBracket 𝕜 V W x :=
  by
  simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ] at hW ⊢
  exact lieBracketWithin_const_smul_right hW uniqueDiffWithinAt_univ

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