Theorems · Theorem · general topology

nhdsWithin_of_mem_discrete

∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s → ∀ {x : X}, x ∈ s → nhdsWithin x s = pure x

The neighbourhoods filter of x within s, under the discrete topology, is equal to the pure x filter (which is the principal filter at the singleton {x}.)

Defined in

Mathlib.Topology.Separation.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace