Theorems · Theorem · Lie groups

mulInvariantVector_mlieBracket

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] [LieGroup I (minSmoothness 𝕜 3) G]
  [CompleteSpace E] (v w : GroupLieAlgebra I G),
  mulInvariantVectorField (VectorField.mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) =
    VectorField.mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)

The invariant vector field associated to the value at the identity of the Lie bracket of two invariant vector fields, is everywhere the Lie bracket of the invariant vector fields.

Defined in

Mathlib.Geometry.Manifold.GroupLieAlgebra

Cited by

0 results in Mathlib

Foundations

Depth 230 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldTopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceChartedSpaceGroupLieGroupCompleteSpace