English
A refined version of pullback compatibility with the Lie bracket under a differentiable map f, with additional hypotheses ensuring smoothness.
Русский
Уточненная версия совместимости подвода со скобкой Ли при дифференцируемом отображении f, с дополнительными предпосылками гладкости.
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
theorem mlieBracketWithin_eq_mlieBracket (hs : UniqueMDiffWithinAt I s x)
(hV : MDifferentiableAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) x)
(hW : MDifferentiableAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) x) :
mlieBracketWithin I V W s x = mlieBracket I V W x :=
by
simp only [← mlieBracketWithin_univ, ← mdifferentiableWithinAt_univ] at hV hW ⊢
exact mlieBracketWithin_subset (subset_univ _) hs hV hW
