Theorems · Theorem · general topology

biInter_basis_nhds

∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {x : X},
  (nhds x).HasBasis p s → ⋂ i, ⋂ (_ : p i), s i = {x}

Defined in

Mathlib.Topology.Separation.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT1Space