Theorems · Definition · general topology

EMetricSpace.toMetricSpace

{α : Type u} → [inst : EMetricSpace α] → (∀ (x y : α), edist x y ≠ ⊤) → MetricSpace α

One gets a metric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the metric space and the emetric space.

Defined in

Mathlib.Topology.MetricSpace.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

EMetricSpace