English
For any v in GroupLieAlgebra I G, the map g ↦ (mulInvariantVectorField v g) is MDifferentiable from I to I.tangent, i.e., the invariant vector field depends MDifferentiably on the group parameter.
Русский
Для любого v из GroupLieAlgebra I G отображение g ↦ mulInvariantVectorField v g является MDifferentiable между геометриями I и TangentBundle I G, т.е. инвариантное векторное поле зависит MD differentiably от параметра группы.
LaTeX
$$$MDifferentiable\, I\, I.tangent\, (\lambda g. (mulInvariantVectorField\, v\, g : TangentBundle I G))$$$
Lean4
@[to_additive]
theorem mdifferentiable_mulInvariantVectorField (v : GroupLieAlgebra I G) :
MDifferentiable I I.tangent (fun (g : G) ↦ (mulInvariantVectorField v g : TangentBundle I G)) :=
(contMDiff_mulInvariantVectorField v).mdifferentiable (le_trans (by simp) le_minSmoothness)