English
Right-scalar smul: the bracket with c•W is c times the bracket with W, under differentiability and unique diff conditions.
Русский
Правый множитель на скаляр: скобка с c•W равна c умноженному на скобку с W при необходимых условиях.
LaTeX
$$Theorem mlieBracketWithin_const_smul_right (hW : MDifferentiableWithinAt I I.tangent (fun x => (W x : TangentBundle I M)) s x) (hs : UniqueMDiffWithinAt I s x) : mlieBracketWithin I V (c • W) s x = c • mlieBracketWithin I V W s x$$
Lean4
theorem mlieBracketWithin_const_smul_right
(hW : MDifferentiableWithinAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) s x)
(hs : UniqueMDiffWithinAt I s x) : mlieBracketWithin I V (c • W) s x = c • mlieBracketWithin I V W s x :=
by
simp only [mlieBracketWithin_apply]
rw [← ContinuousLinearMap.map_smul, mpullbackWithin_smul, lieBracketWithin_const_smul_right]
· exact hW.differentiableWithinAt_mpullbackWithin_vectorField
· exact uniqueMDiffWithinAt_iff_inter_range.1 hs
