English
If U and V are ContMDiffWithinAt of order n, and hmn holds, then mlieBracketWithin is ContMDiffWithinAt of order m.
Русский
Если U и V — ContMDiffWithinAt порядка n, и условие гладкости выполняется, то mlieBracketWithin гладок порядка m.
LaTeX
$$$\mathrm{ContMDiffWithinAt} \; I I\textrm{ tangent } \; m \; (\lambda x. (U x)) \; s x \; \Rightarrow \; \mathrm{ContMDiffWithinAt} \; I I\textrm{ tangent } m \; (\lambda x. (\mathrm{mlieBracketWithin}(I, U, V, s, x)))$$$
Lean4
theorem mpullback_mlieBracket {f : M → M'} {V W : Π (x : M'), TangentSpace I' x} {x₀ : M}
(hV : MDifferentiableAt I' I'.tangent (fun x ↦ (V x : TangentBundle I' M')) (f x₀))
(hW : MDifferentiableAt I' I'.tangent (fun x ↦ (W x : TangentBundle I' M')) (f x₀)) (hf : ContMDiffAt I I' n f x₀)
(hn : minSmoothness 𝕜 2 ≤ n) :
mpullback I I' f (mlieBracket I' V W) x₀ = mlieBracket I (mpullback I I' f V) (mpullback I I' f W) x₀ :=
by
simp only [← mlieBracketWithin_univ, ← mdifferentiableWithinAt_univ] at hV hW ⊢
exact mpullback_mlieBracketWithin hV hW uniqueMDiffOn_univ hf (mem_univ _) hn (by simp)
