Theorems · Theorem · general topology

TopologicalSpace.nhds_mkOfNhds_of_hasBasis

∀ {α : Type u} {n : α → Filter α} {ι : α → Sort u_1} {p : (a : α) → ι a → Prop} {s : (a : α) → ι a → Set α},
  (∀ (a : α), (n a).HasBasis (p a) (s a)) →
    (∀ (a : α) (i : ι a), p a i → a ∈ s a i) →
      (∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x) → ∀ (a : α), nhds a = n a

Defined in

Mathlib.Topology.Order

Cited by

5 results in Mathlib

Foundations

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