lieBracketWithin_vectorField_eq_of_mem

English

If V₁ =ᶠ[𝓝 x] V and W₁ =ᶠ[𝓝 x] W, then lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x.

Русский

Если V₁ эквивалентно V в окрестности x и W₁ эквивалентно W, то скобка Ли между V₁ и W₁ в x равна скобке между V и W в x.

LaTeX

$$$(hV: V₁ =ᶠ[𝓝 x] V) \\land (hW: W₁ =ᶠ[𝓝 x] W) \\Rightarrow lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x$$$

Lean4

theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem (hV : V₁ =ᶠ[𝓝[s] x] V) (hW : W₁ =ᶠ[𝓝[s] x] W)
    (hx : x ∈ s) : lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x :=
  hV.lieBracketWithin_vectorField_eq (mem_of_mem_nhdsWithin hx hV :) hW (mem_of_mem_nhdsWithin hx hW :)

Похожие утверждения