Theorems · Theorem · general topology

nhdsWithin_eq_comap_uniformity_of_mem

∀ {α : Type ua} [inst : UniformSpace α] {x : α} {T : Set α},
  x ∈ T → ∀ (S : Set α), nhdsWithin x S = Filter.comap (Prod.mk x) (uniformity α ⊓ Filter.principal (T ×ˢ S))

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace