mlieBracketWithin_vectorField_of_insert

English

If V₁ and W₁ are equal to V and W on nhds x, then the values of the Lie bracket at x agree: mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x.

Русский

Если V₁=V и W₁=W на окрестности x, то значения скобки совпадают.

LaTeX

$$$ (nhds x).EventuallyEq V₁ V \to (nhds x).EventuallyEq W₁ W \to mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x $$$

Lean4

protected theorem _root_.Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert (hV : V₁ =ᶠ[𝓝[insert x s] x] V)
    (hW : W₁ =ᶠ[𝓝[insert x s] x] W) : mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x := by
  apply mem_of_mem_nhdsWithin (mem_insert x s) (hV.mlieBracketWithin_vectorField' hW (subset_insert x s))

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