Theorems · Theorem · general topology

nhds_basis_opens

∀ {X : Type u} [inst : TopologicalSpace X] (x : X), (nhds x).HasBasis (fun s => x ∈ s ∧ IsOpen s) fun s => s

The open sets containing x are a basis for the neighborhood filter. See nhds_basis_opens' for a variant using open neighborhoods instead.

Defined in

Mathlib.Topology.Neighborhoods

Cited by

54 results in Mathlib

Foundations

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

Assumes

TopologicalSpace