mdifferentiable_mulInvariantVectorField

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)

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