Theorems · Theorem · general topology

UniformSpace.Completion.mem_uniformity_dist

∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set (UniformSpace.Completion α × UniformSpace.Completion α)),
  s ∈ uniformity (UniformSpace.Completion α) ↔ ∃ ε > 0, ∀ {a b : UniformSpace.Completion α}, dist a b < ε → (a, b) ∈ s

Elements of the uniformity (defined generally for completions) can be characterized in terms of the distance.

Defined in

Mathlib.Topology.MetricSpace.Completion

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace