contMDiffAt_mulInvariantVectorField

English

Let v be a fixed element of the group Lie algebra of I on G. For every g in G, the map g ↦ mulInvariantVectorField v g is ContMDiffAt I I.tangent with smoothness minSmoothness 𝕜 2.

Русский

Пусть v — фиксированный элемент из групповой Ли-алгебры I на G. Для каждого g ∈ G отображение g ↦ mulInvariantVectorField v g является ContMDiffAt I I.tangent с гладкостью не менее minSmoothness 𝕜 2.

LaTeX

$$$ContMDiffAt\, I\, I.tangent\, (\minSmoothness\, 𝕜\, 2)\, (\lambda g. (mulInvariantVectorField\, v\, g : TangentBundle I G))\, g$$$

Lean4

@[to_additive]
theorem contMDiffAt_mulInvariantVectorField (v : GroupLieAlgebra I G) {g : G} :
    ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun (g : G) ↦ (mulInvariantVectorField v g : TangentBundle I G)) g :=
  (contMDiff_mulInvariantVectorField v).contMDiffAt

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