English
If V and W are differentiable within s at x, then the bracket coincides with the global bracket at x.
Русский
Если V и W дифференцируемы внутри s в точке x, то скобка совпадает с глобальной скобкой в x.
LaTeX
$$$\mathrm{mlieBracketWithin}(I, V, W, s, x) = \mathrm{mlieBracket}(I, V, W)(x)$$$
Lean4
theorem mlieBracketWithin_of_mem_nhdsWithin (st : t ∈ 𝓝[s] x) (hs : UniqueMDiffWithinAt I s x)
(hV : MDifferentiableWithinAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) t x)
(hW : MDifferentiableWithinAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) t x) :
mlieBracketWithin I V W s x = mlieBracketWithin I V W t x :=
by
simp only [mlieBracketWithin_apply]
congr 1
rw [lieBracketWithin_of_mem_nhdsWithin]
· apply Filter.inter_mem
· apply nhdsWithin_mono _ inter_subset_left
exact (continuousAt_extChartAt_symm x).continuousWithinAt.preimage_mem_nhdsWithin'' st (by simp)
· exact nhdsWithin_mono _ inter_subset_right self_mem_nhdsWithin
· exact uniqueMDiffWithinAt_iff_inter_range.1 hs
· exact hV.differentiableWithinAt_mpullbackWithin_vectorField
· exact hW.differentiableWithinAt_mpullbackWithin_vectorField
