Theorems · Theorem · general topology

mem_uniformity_edist

∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set (α × α)},
  s ∈ uniformity α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s

Characterization of the elements of the uniformity in terms of the extended distance

Defined in

Mathlib.Topology.EMetricSpace.Defs

Cited by

6 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace