English
Let V and V1 be vector fields differentiable within a set s near x, and W be another vector field. Then [V+V1, W] = [V, W] + [V1, W] on s near x.
Русский
Пусть V и V1 — векторные поля, дифференцируемые внутри множества s около x, и W другое поле. Тогда [V+V1, W] = [V, W] + [V1, W] на s около x.
LaTeX
$$$\mathrm{mlieBracketWithin}(I, V+V_1, W, s, x) = \mathrm{mlieBracketWithin}(I, V, W, s, x) + \mathrm{mlieBracketWithin}(I, V_1, W, s, x)$$$
Lean4
theorem mlieBracketWithin_add_left (hV : MDifferentiableWithinAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) s x)
(hV₁ : MDifferentiableWithinAt I I.tangent (fun x ↦ (V₁ x : TangentBundle I M)) s x)
(hs : UniqueMDiffWithinAt I s x) :
mlieBracketWithin I (V + V₁) W s x = mlieBracketWithin I V W s x + mlieBracketWithin I V₁ W s x :=
by
simp only [mlieBracketWithin_apply]
rw [← ContinuousLinearMap.map_add, mpullbackWithin_add, lieBracketWithin_add_left]
· exact hV.differentiableWithinAt_mpullbackWithin_vectorField
· exact hV₁.differentiableWithinAt_mpullbackWithin_vectorField
· exact uniqueMDiffWithinAt_iff_inter_range.1 hs
