Theorems · Theorem · general topology

eventually_nhds_iff

∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {p : X → Prop},
  (∀ᶠ (y : X) in nhds x, p y) ↔ ∃ t, (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t

A predicate is true in a neighborhood of x iff it is true for all the points in an open set containing x.

Defined in

Mathlib.Topology.Neighborhoods

Cited by

21 results in Mathlib

Foundations

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

Assumes

TopologicalSpace