English
The Lie bracket of vector fields satisfies the Leibniz identity inside a set under suitable differentiability assumptions: [U, [V, W]] = [[U, V], W] + [V, [U, W]] at x.
Русский
Скобка Ли векторных полей удовлетворяет тождеству Лейбница внутри множества при надлежащей дифференцируемости: [U,[V,W]] = [[U,V],W] + [V,[U,W]] в точке x.
LaTeX
$$$ lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x = lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x $$$
Lean4
/-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]`. -/
theorem leibniz_identity_lieBracket (hn : minSmoothness 𝕜 2 ≤ n) {U V W : E → E} {x : E} (hU : ContDiffAt 𝕜 n U x)
(hV : ContDiffAt 𝕜 n V x) (hW : ContDiffAt 𝕜 n W x) :
lieBracket 𝕜 U (lieBracket 𝕜 V W) x = lieBracket 𝕜 (lieBracket 𝕜 U V) W x + lieBracket 𝕜 V (lieBracket 𝕜 U W) x :=
by
simp only [← lieBracketWithin_univ, ← contDiffWithinAt_univ] at hU hV hW ⊢
exact leibniz_identity_lieBracketWithin hn uniqueDiffOn_univ (by simp) (mem_univ _) hU hV hW
