English
If U and V are ContMDiffOn within a set s, then mlieBracketWithin is ContMDiffOn on s.
Русский
Если U и V — ContMDiffOn внутри множества s, то mlieBracketWithin на s гладок.
LaTeX
$$$\mathrm{ContMDiffOn}(I, I.tangent, n, (x \mapsto (U x))) s \Rightarrow \mathrm{ContMDiffOn}(I, I.tangent, m, (x \mapsto (\mathrm{mlieBracketWithin}(I, U, V, s, x)))) s$$$
Lean4
/-- If two vector fields are `C^n` with `n ≥ m + 1`, then their Lie bracket is `C^m`. -/
theorem _root_.ContMDiffAt.mlieBracket_vectorField {m n : ℕ∞} [IsManifold I (n + 1) M]
{U V : Π (x : M), TangentSpace I x} {x : M} (hU : ContMDiffAt I I.tangent n (fun x ↦ (U x : TangentBundle I M)) x)
(hV : ContMDiffAt I I.tangent n (fun x ↦ (V x : TangentBundle I M)) x) (hmn : minSmoothness 𝕜 (m + 1) ≤ n) :
ContMDiffAt I I.tangent m (fun x ↦ (mlieBracket I U V x : TangentBundle I M)) x :=
by
simp only [← contMDiffWithinAt_univ, ← mlieBracketWithin_univ] at hU hV ⊢
exact hU.mlieBracketWithin_vectorField hV uniqueMDiffOn_univ (mem_univ _) hmn
