English
Let V1 and V be vector fields and W1 and W be vector fields such that V1 and V agree at x in the neighborhood nhds x (respecting the notion of eventual equality), and likewise W1 and W agree near x. Then the Lie bracket of V1 with W1 agrees with the Lie bracket of V with W in nhds x; i.e., lieBracket 𝕜 V1 W1 =ᶠ[𝓝 x] lieBracket 𝕜 V W.
Русский
Пусть векторные поля V1 и V, W1 и W согласуются окрестности точки x (в смысле предельной эквивалентности на 𝓝 x). Тогда скобка Ли между V1 и W1 совпадает с скобкой Ли между V и W ближje к x: lieBracket 𝕜 V1 W1 =ᶠ[𝓝 x] lieBracket 𝕜 V W.
LaTeX
$$$ lieBracket 𝕜 V₁ W₁ =ᶠ[𝓝 x] lieBracket 𝕜 V W $$$
Lean4
protected theorem _root_.Filter.EventuallyEq.lieBracket_vectorField (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) :
lieBracket 𝕜 V₁ W₁ =ᶠ[𝓝 x] lieBracket 𝕜 V W :=
by
filter_upwards [hV.eventuallyEq_nhds, hW.eventuallyEq_nhds] with y hVy hWy
exact hVy.lieBracket_vectorField_eq hWy
