Extending local identities from dense sets

Two maps into a Hausdorff space that are continuous near a point and agree near that point within a dense set agree on a full neighborhood. In particular, this extends identities across a coordinate hyperplane when its complement is dense.

theorem Dense.eventuallyEq_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {s : Set X} {x : X} {f g : X → Y} (hs : Dense s) (hf : ∀ᶠ (z : X) in nhds x, ContinuousAt f z) (hg : ∀ᶠ (z : X) in nhds x, ContinuousAt g z) (hfg : f =ᶠ[nhdsWithin x s] g) : f =ᶠ[nhds x] g

Maps that are continuous near a point and agree near it within a dense set agree on a full neighborhood of the point.