lieBracketWithin_add_right — Mathlib

English

lieBracketWithin 𝕜 V (W + W1) s x = lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V W1 s x when W, W1 differentiable at x.

Русский

При сумме справа: [V, W+W1]_s(x) = [V,W]_s(x) + [V,W1]_s(x).

LaTeX

$$$\operatorname{lieBracketWithin} 𝕜 V (W + W_1) s x = \operatorname{lieBracketWithin} 𝕜 V W s x + \operatorname{lieBracketWithin} 𝕜 V W_1 s x$$$

Lean4

theorem lieBracketWithin_add_right (hW : DifferentiableWithinAt 𝕜 W s x) (hW₁ : DifferentiableWithinAt 𝕜 W₁ s x)
    (hs : UniqueDiffWithinAt 𝕜 s x) :
    lieBracketWithin 𝕜 V (W + W₁) s x = lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V W₁ s x :=
  by
  simp only [lieBracketWithin, Pi.add_apply, map_add]
  rw [fderivWithin_add hs hW hW₁, ContinuousLinearMap.add_apply]
  abel

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