mlieBracketWithin_congr — Mathlib

English

If s,t are equivalent on nhds x, then the two bracket expressions coincide at x.

Русский

Если s и t совпадают в окрестности x, скобочные выражения совпадают в x.

LaTeX

$$$(nhds x).EventuallyEq s t \Rightarrow mlieBracketWithin I V W s x = mlieBracketWithin I V W t x$$$

Lean4

theorem mlieBracketWithin_congr (hV : EqOn V₁ V s) (hVx : V₁ x = V x) (hW : EqOn W₁ W s) (hWx : W₁ x = W x) :
    mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x :=
  (hV.eventuallyEq.filter_mono inf_le_right).mlieBracketWithin_vectorField_eq hVx
    (hW.eventuallyEq.filter_mono inf_le_right) hWx

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