lieBracketWithin_eventually_congr_set'

English

If s and t coincide in nhds of x except at most one point, then lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x.

Русский

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

LaTeX

$$$(y: E) \\Rightarrow lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x$$$

Lean4

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

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