Theorems · Theorem · general topology

Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete

∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} {p : ι → Prop} {t : ι → Set X} {s : Set X},
  IsDiscrete s → ∀ {x : X}, (nhds x).HasBasis p t → x ∈ s → ∃ i, p i ∧ t i ∩ s = {x}

Defined in

Mathlib.Topology.Separation.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpace