Theorems · Theorem · general topology

Filter.HasBasis.specializes_iff

∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {ι : Sort u_7} {p : ι → Prop} {s : ι → Set X},
  (nhds y).HasBasis p s → (x ⤳ y ↔ ∀ (i : ι), p i → x ∈ s i)

Defined in

Mathlib.Topology.Inseparable

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpace