mlieBracket_add_left — Mathlib

English

Linearity of the Lie bracket in the first argument: [V+V1, W] = [V, W] + [V1, W] at x.

Русский

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

LaTeX

$$$\mathrm{mlieBracket}(I, V+V_1, W)(x) = \mathrm{mlieBracket}(I, V, W)(x) + \mathrm{mlieBracket}(I, V_1, W)(x)$$$

Lean4

theorem mlieBracket_add_left (hV : MDifferentiableAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) x)
    (hV₁ : MDifferentiableAt I I.tangent (fun x ↦ (V₁ x : TangentBundle I M)) x) :
    mlieBracket I (V + V₁) W x = mlieBracket I V W x + mlieBracket I V₁ W x :=
  by
  simp only [← mlieBracketWithin_univ] at hV hV₁ ⊢
  exact mlieBracketWithin_add_left hV hV₁ (uniqueMDiffWithinAt_univ _)

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