English
In the constant-field case, the bracket vanishes, illustrating the pullback compatibility in a simple instance.
Русский
В случае константных полей скобка обращается в ноль, иллюстрируя совместимость pullback в простом примере.
LaTeX
$$$ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x = 0 $$$
Lean4
/-- The Lie bracket commutes with taking pullbacks. One could also give a version avoiding
completeness but requiring that `f` is a local diffeo. -/
theorem pullback_lieBracket (hn : minSmoothness 𝕜 2 ≤ n) {f : E → F} {V W : F → F} {x : E} (h'f : ContDiffAt 𝕜 n f x)
(hV : DifferentiableAt 𝕜 V (f x)) (hW : DifferentiableAt 𝕜 W (f x)) :
pullback 𝕜 f (lieBracket 𝕜 V W) x = lieBracket 𝕜 (pullback 𝕜 f V) (pullback 𝕜 f W) x :=
pullback_lieBracket_of_isSymmSndFDerivAt (h'f.isSymmSndFDerivAt hn) (h'f.of_le (le_minSmoothness.trans hn)) hV hW
