mlieBracket_add_right — Mathlib

English

If the differentiability of V and W holds on a larger neighborhood t containing the original s near x, then the value at x is the same when computed using s or t.

Русский

Если V и W дифференцируемы на большем окне t, содержащем s рядом с x, то значение скобки в x одинаково, независимо от использования s или t.

LaTeX

$$$\mathrm{mlieBracketWithin}(I, V, W, s, x) = \mathrm{mlieBracketWithin}(I, V, W, t, x)$$$

Lean4

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

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