mlieBracketWithin_vectorField_eq_nhds

English

If V₁ ≡ V and W₁ ≡ W eventually on nhds x, then mlieBracketWithin I V₁ W₁ s x ≡ mlieBracketWithin I V W s x on nhds x.

Русский

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

LaTeX

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

Lean4

theorem _root_.Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_nhds (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) :
    mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x :=
  (hV.filter_mono nhdsWithin_le_nhds).mlieBracketWithin_vectorField_eq hV.self_of_nhds
    (hW.filter_mono nhdsWithin_le_nhds) hW.self_of_nhds

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