lieBracketWithin_vectorField_eq_nhds

English

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

Русский

Если V₁ эквивалентно V по 𝓝 x и W₁ эквивалентно W по 𝓝 x, то локальная скобка внутри s равна обычной для V и W.

LaTeX

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

Lean4

theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField_eq_nhds (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) :
    lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x :=
  (hV.filter_mono nhdsWithin_le_nhds).lieBracketWithin_vectorField_eq hV.self_of_nhds
    (hW.filter_mono nhdsWithin_le_nhds) hW.self_of_nhds

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