English
If nhds x makes V₁ ≈ V and W₁ ≈ W, then the Lie bracket at x agrees: lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x.
Русский
Если окрестность x заставляет V₁ быть эквивалентным V и W₁ эквивалентным W, тогда скобка Ли в x совпадает:lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x.
LaTeX
$$$(hV: V₁ =ᶠ[𝓝 x] V) \\land (hW: W₁ =ᶠ[𝓝 x] W) \\Rightarrow lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x$$$
Lean4
/-- If vector fields coincide on a neighborhood of a point within a set, then the Lie brackets
also coincide on a neighborhood of this point within this set. Version where one considers the Lie
bracket within a subset. -/
theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField' (hV : V₁ =ᶠ[𝓝[s] x] V) (hW : W₁ =ᶠ[𝓝[s] x] W)
(ht : t ⊆ s) : lieBracketWithin 𝕜 V₁ W₁ t =ᶠ[𝓝[s] x] lieBracketWithin 𝕜 V W t :=
by
filter_upwards [hV.fderivWithin' ht (𝕜 := 𝕜), hW.fderivWithin' ht (𝕜 := 𝕜), hV, hW] with x hV' hW' hV hW
simp [lieBracketWithin, hV', hW', hV, hW]
