English
The invariant vector field corresponding to the value at identity of the Lie bracket of two invariant vector fields satisfies a bracket identity: the invariant vector field of the Lie bracket equals the Lie bracket of the invariant vector fields themselves.
Русский
Инвариантное векторное поле, соответствующее значение в точке идентичности скобки Ли двух инвариантных векторных полей, равняется скобке Ли между соответствующими инвариантными векторными полями.
LaTeX
$$$mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) = mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)$$$
Lean4
@[to_additive]
theorem mdifferentiableAt_mulInvariantVectorField (v : GroupLieAlgebra I G) {g : G} :
MDifferentiableAt I I.tangent (fun (g : G) ↦ (mulInvariantVectorField v g : TangentBundle I G)) g :=
(contMDiffAt_mulInvariantVectorField v).mdifferentiableAt (le_trans (by simp) le_minSmoothness)
