Theorems · Theorem · general topology

nhds_basis_uniformity

∀ {α : Type ua} {ι : Sort u_1} [inst : UniformSpace α] {p : ι → Prop} {s : ι → SetRel α α},
  (uniformity α).HasBasis p s → ∀ {x : α}, (nhds x).HasBasis p fun i => {y | (y, x) ∈ s i}

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

21 results in Mathlib

Foundations

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

Assumes

UniformSpace