English
If U, V are differentiable in a neighborhood, then the Lie bracket [U, V] is differentiable in a neighborhood with appropriately reduced smoothness.
Русский
Если U, V дифференцируемы в окрестности, то скобка Ли [U, V] дифференцируема в окрестности с уменьшенной гладкостью.
LaTeX
$$$\text{ContMDiffWithinAt}(I, \mathrm{tangent}, m, (U \,\cdot) ) \Rightarrow \mathrm{mlieBracketWithin}(I, U, V, s, x) \text{ is ContMDiffSince...}$$$
Lean4
/-- The pullback commutes with the Lie bracket of vector fields on manifolds. -/
theorem mpullbackWithin_mlieBracketWithin {f : M → M'} {V W : Π (x : M'), TangentSpace I' x} {x₀ : M} {s : Set M}
{t : Set M'} (hV : MDifferentiableWithinAt I' I'.tangent (fun x ↦ (V x : TangentBundle I' M')) t (f x₀))
(hW : MDifferentiableWithinAt I' I'.tangent (fun x ↦ (W x : TangentBundle I' M')) t (f x₀)) (hu : UniqueMDiffOn I s)
(hf : ContMDiffWithinAt I I' n f s x₀) (hx₀ : x₀ ∈ s) (hn : minSmoothness 𝕜 2 ≤ n) (hst : f ⁻¹' t ∈ 𝓝[s] x₀)
(h'x₀ : x₀ ∈ closure (interior s)) :
mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ =
mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀ :=
mpullbackWithin_mlieBracketWithin' hV hW hu hu hf hx₀ hn hst h'x₀ Subset.rfl
