update_eventuallyEq_nhdsNE — Mathlib

English

The update of f at a by b equals f eventually with respect to the punctured neighborhood of a'.

Русский

Обновление f в точке a до значения b эквивалентно f выполнимо в окрестностях точки a' с пропуском точки.

LaTeX

$$$ \\mathrm{update}(f, a, b) =^{\\mathcal{N}_{\\neq a'}} f. $$$

Lean4

theorem update_eventuallyEq_nhdsNE {α β : Type*} [TopologicalSpace α] [T1Space α] [DecidableEq α] (f : α → β) (a a' : α)
    (b : β) : Function.update f a b =ᶠ[𝓝[≠] a'] f :=
  (Function.update_eventuallyEq_cofinite f a b).filter_mono (nhdsNE_le_cofinite a')

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