Theorems · Theorem · general topology

TopologicalSpace.IsTopologicalBasis.nhds_hasBasis

∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis b → ∀ {a : α}, (nhds a).HasBasis (fun t => t ∈ b ∧ a ∈ t) fun t => t

Defined in

Mathlib.Topology.Bases

Cited by

10 results in Mathlib

Foundations

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

Assumes

TopologicalSpace