lieBracket_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{lieBracket}(V+V1, W) = \mathrm{lieBracket}(V, W) + \mathrm{lieBracket}(V1, W).$$$

Lean4

theorem lieBracket_add_left (hV : DifferentiableAt 𝕜 V x) (hV₁ : DifferentiableAt 𝕜 V₁ x) :
    lieBracket 𝕜 (V + V₁) W x = lieBracket 𝕜 V W x + lieBracket 𝕜 V₁ W x :=
  by
  simp only [lieBracket, Pi.add_apply, map_add]
  rw [fderiv_add hV hV₁, ContinuousLinearMap.add_apply]
  abel

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