English
Under a smooth map, the pullback of the Lie bracket equals the Lie bracket of the pullbacks.
Русский
При гладком отображении подстановка через сопоставление: подстановочная скобка Ли равна скобке подстановок.
LaTeX
$$$\mathrm{mpullbackWithin}(I, I', f, \mathrm{mlieBracketWithin}(I', V, W, t), s, x_0) = \mathrm{mlieBracketWithin}(I, \mathrm{mpullbackWithin}(I, I', f, V, s), \mathrm{mpullbackWithin}(I, I', f, W, s), s, x_0)$$$
Lean4
/-- If two vector fields are `C^n` with `n ≥ m + 1`, then their Lie bracket is `C^m`. -/
theorem _root_.ContMDiffOn.mlieBracketWithin_vectorField {m n : ℕ∞} [IsManifold I (n + 1) M]
{U V : Π (x : M), TangentSpace I x} (hU : ContMDiffOn I I.tangent n (fun x ↦ (U x : TangentBundle I M)) s)
(hV : ContMDiffOn I I.tangent n (fun x ↦ (V x : TangentBundle I M)) s) (hs : UniqueMDiffOn I s)
(hmn : minSmoothness 𝕜 (m + 1) ≤ n) :
ContMDiffOn I I.tangent m (fun x ↦ (mlieBracketWithin I U V s x : TangentBundle I M)) s := fun x hx ↦
(hU x hx).mlieBracketWithin_vectorField (hV x hx) hs hx hmn
