Structures · Topology

EMetricSpace

An extended metric space is a type endowed with a ℝ≥0∞-valued distance edist satisfying edist x y = 0 ↔ x = y, commutativity edist x y = edist y x, and the triangle inequality edist x z ≤ edist x y + edist y z. See pseudo extended metric spaces (PseudoEMetricSpace) for the similar class with the edist x y = 0 ↔ x = y assumption weakened to edist x x = 0. Any extended metric space is a T1 topological space and a uniform space (see TopologicalSpace, T1Space, UniformSpace), where the topology and uniformity come from the metric. We make the uniformity/topology part of the data instead of deriving it from the metric. This e.g. ensures that we do not get a diamond when doing [EMetricSpace α] [EMetricSpace β] : TopologicalSpace (α × β): The product metric and product topology agree, but not definitionally so. See Note [forgetful inheritance].