mlieBracketWithin_eq_lieBracketWithin

English

The equivalence of Lie bracket definitions: the within-definition coincides with the general bracket definition on model spaces.

Русский

Эквивалентность определений скобки Ли: внутри-определение совпадает с общим определением скобки на модельных пространствах.

LaTeX

$$VectorField.mlieBracketWithin_eq_lieBracketWithin I V W s = lieBracketWithin 𝕜 V W s$$

Lean4

theorem mlieBracketWithin_eq_lieBracketWithin {V W : Π (x : E), TangentSpace 𝓘(𝕜, E) x} {s : Set E} :
    mlieBracketWithin 𝓘(𝕜, E) V W s = lieBracketWithin 𝕜 V W s :=
  by
  ext x
  simp [mlieBracketWithin_apply]
    /- Copy of the `lieBracket` API to manifolds -/

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