Structures · Topology

PseudoEMetricSpace

A pseudo extended metric space is a type endowed with a ℝ≥0∞-valued distance edist satisfying reflexivity edist x x = 0, commutativity edist x y = edist y x, and the triangle inequality edist x z ≤ edist x y + edist y z. Note that we do not require edist x y = 0 → x = y. See extended metric spaces (EMetricSpace) for the similar class with that stronger assumption. Any pseudo extended metric space is a topological space and a uniform space (see TopologicalSpace, UniformSpace), where the topology and uniformity come from the metric. Note that a T1 pseudo extended metric space is just an extended metric space. 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 [PseudoEMetricSpace α] [PseudoEMetricSpace β] : TopologicalSpace (α × β): The product metric and product topology agree, but not definitionally so. See Note [forgetful inheritance].

Defined in

Mathlib.Topology.EMetricSpace.Defs

Shape

One type argument · adds edist_self, edist_comm, edist_triangle, toUniformSpace, uniformity_edist