Theorems · Theorem · general topology

nhds_nhds_eq_uniformity_uniformity_prod

∀ {α : Type ua} [inst : UniformSpace α] {a b : α},
  nhds a ×ˢ nhds b = (uniformity α).lift fun s => (uniformity α).lift' fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace