English
Jacobi/leibniz identities for brackets with multiple vector fields exhibit linearity properties.
Русский
Идентичности Якоби/Лейбница для скобок с несколькими векторными полями демонстрируют линейность.
LaTeX
$$$\mathrm{leibnizIdentity}(U,V,W) : [U, [V, W]] = [[U, V], W] + [V, [U, W]]$$$
Lean4
/-- The Lie bracket of vector fields in manifolds satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]` (also called Jacobi identity). -/
theorem leibniz_identity_mlieBracket {U V W : Π (x : M), TangentSpace I x}
(hU : ContMDiff I I.tangent (minSmoothness 𝕜 2) (fun x ↦ (U x : TangentBundle I M)))
(hV : ContMDiff I I.tangent (minSmoothness 𝕜 2) (fun x ↦ (V x : TangentBundle I M)))
(hW : ContMDiff I I.tangent (minSmoothness 𝕜 2) (fun x ↦ (W x : TangentBundle I M))) :
mlieBracket I U (mlieBracket I V W) = mlieBracket I (mlieBracket I U V) W + mlieBracket I V (mlieBracket I U W) :=
by
ext x
exact leibniz_identity_mlieBracket_apply (hU x) (hV x) (hW x)
