mlieBracket_vectorField — Mathlib

English

Variant: if sets s,t agree outside a point y then the Lie bracket within s and t agree on nhds around x.

Русский

Вариант: если s,t совпадают вне точки y, то скобка внутри s и t совпадают на окрестности x.

LaTeX

$$Theorem mlieBracketWithin_congr_set' (y: M) (h: s =ᶠ[𝓝[{ y }ᶜ] x] t) : mlieBracketWithin I V W s x = mlieBracketWithin I V W t x$$

Lean4

protected theorem _root_.Filter.EventuallyEq.mlieBracket_vectorField (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) :
    mlieBracket I V₁ W₁ =ᶠ[𝓝 x] mlieBracket I V W :=
  by
  filter_upwards [hV.eventuallyEq_nhds, hW.eventuallyEq_nhds] with y hVy hWy
  exact hVy.mlieBracket_vectorField_eq hWy

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