lieBracketWithin_vectorField — Mathlib

English

If nhds x satisfies V₁ ≈ V and W₁ ≈ W, then lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x.

Русский

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

LaTeX

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

Lean4

protected theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField (hV : V₁ =ᶠ[𝓝[s] x] V)
    (hW : W₁ =ᶠ[𝓝[s] x] W) : lieBracketWithin 𝕜 V₁ W₁ s =ᶠ[𝓝[s] x] lieBracketWithin 𝕜 V W s :=
  hV.lieBracketWithin_vectorField' hW Subset.rfl

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