lieBracketWithin_vectorField_eq_of_insert

English

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

Русский

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

LaTeX

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

Lean4

protected theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_insert (hV : V₁ =ᶠ[𝓝[insert x s] x] V)
    (hW : W₁ =ᶠ[𝓝[insert x s] x] W) : lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x := by
  apply mem_of_mem_nhdsWithin (mem_insert x s) (hV.lieBracketWithin_vectorField' hW (subset_insert x s))

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