lieBracketWithin_vectorField_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField_eq (hV : V₁ =ᶠ[𝓝[s] x] V) (hxV : V₁ x = V x)
    (hW : W₁ =ᶠ[𝓝[s] x] W) (hxW : W₁ x = W x) : lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x := by
  simp only [lieBracketWithin, hV.fderivWithin_eq hxV, hW.fderivWithin_eq hxW, hxV, hxW]

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