lieBracketWithin_add_left — Mathlib

English

Lie bracket is additive in the first argument: [V+V1, W] = [V, W] + [V1, W].

Русский

Скобка Ли линейна по первому аргументу: [V+V1, W] = [V, W] + [V1, W].

LaTeX

$$$\mathrm{lieBracketWithin}(V+V1, W) = \mathrm{lieBracketWithin}(V, W) + \mathrm{lieBracketWithin}(V1, W).$$$

Lean4

theorem lieBracketWithin_add_left (hV : DifferentiableWithinAt 𝕜 V s x) (hV₁ : DifferentiableWithinAt 𝕜 V₁ s x)
    (hs : UniqueDiffWithinAt 𝕜 s x) :
    lieBracketWithin 𝕜 (V + V₁) 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 hV hV₁, ContinuousLinearMap.add_apply]
  abel

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