Theorems · Definition · general topology

nhds

{X : Type u_3} → [TopologicalSpace X] → X → Filter X

A set is called a neighborhood of x if it contains an open set around x. The set of all neighborhoods of x forms a filter, the neighborhood filter at x, is here defined as the infimum over the principal filters of all open sets containing x.

Defined in

Mathlib.Topology.Defs.Filter

Cited by

5,554 results in Mathlib

Foundations

Depth 18 from the axioms, rests on 91 definitions · uses propext, Quot.sound

Assumes

TopologicalSpace