lieBracket_vectorField_eq — Mathlib

English

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

Русский

Если V₁ эквивалентно V по 𝓝 x и W₁ эквивалентно W по 𝓝 x, тогда скобка Ли между 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.lieBracket_vectorField_eq (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) :
    lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x := by
  rw [← lieBracketWithin_univ, ← lieBracketWithin_univ, hV.lieBracketWithin_vectorField_eq_nhds hW]

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