mlieBracketWithin_eventually_congr_set'

English

If two sets s and t are equal outside a point y in a neighborhood sense, then the Lie brackets within s and t are equal near x.

Русский

Если множества s и t совпадают вне точки y в окрестности x, то скобки внутри s и t совпадают близко к x.

LaTeX

$$$s =^\mathcal{N}_{({y})^c} t \Rightarrow \mathrm{mlieBracketWithin}(I,V,W,s,x) = \mathrm{mlieBracketWithin}(I,V,W,t,x)$$$

Lean4

/-- Variant of `mlieBracketWithin_eventually_congr_set` where one requires the sets to coincide only
in the complement of a point. -/
theorem mlieBracketWithin_eventually_congr_set' (y : M) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
    mlieBracketWithin I V W s =ᶠ[𝓝 x] mlieBracketWithin I V W t :=
  (eventually_nhds_nhdsWithin.2 h).mono fun _ => mlieBracketWithin_congr_set' y

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