mlieBracketWithin_add_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mlieBracketWithin_add_right (hW : MDifferentiableWithinAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) s x)
    (hW₁ : MDifferentiableWithinAt I I.tangent (fun x ↦ (W₁ x : TangentBundle I M)) s x)
    (hs : UniqueMDiffWithinAt I s x) :
    mlieBracketWithin I V (W + W₁) s x = mlieBracketWithin I V W s x + mlieBracketWithin I V W₁ s x :=
  by
  rw [mlieBracketWithin_swap, Pi.neg_apply, mlieBracketWithin_add_left hW hW₁ hs, mlieBracketWithin_swap (V := V),
    mlieBracketWithin_swap (V := V), Pi.neg_apply, Pi.neg_apply]
  abel

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