Theorems · Theorem · general topology

Function.update_eventuallyEq_nhdsNE

∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [T1Space α] [inst_2 : DecidableEq α] (f : α → β) (a a' : α)
  (b : β), Function.update f a b =ᶠ[nhdsWithin a' {a'}ᶜ] f

Defined in

Mathlib.Topology.Separation.Basic

Cited by

1 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceT1SpaceDecidableEq