Theorems · Theorem · general topology

Filter.EventuallyEq.eventuallyEq_nhds

∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {f g : X → α},
  f =ᶠ[nhds x] g → ∀ᶠ (y : X) in nhds x, f =ᶠ[nhds y] g

If two functions are equal in a neighbourhood of x, then for y sufficiently close to x these functions are equal in a neighbourhood of y.

Defined in

Mathlib.Topology.Neighborhoods

Cited by

5 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpace