Structures · Topology

PseudoMetricSpace

A pseudometric space is a type endowed with a ℝ-valued distance dist satisfying reflexivity dist x x = 0, commutativity dist x y = dist y x, and the triangle inequality dist x z ≤ dist x y + dist y z. Note that we do not require dist x y = 0 → x = y. See metric spaces (MetricSpace) for the similar class with that stronger assumption. Any pseudometric 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 pseudometric space is just a 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 [PseudoMetricSpace α] [PseudoMetricSpace β] : TopologicalSpace (α × β): The product metric and product topology agree, but not definitionally so. See Note [forgetful inheritance].

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Defs

Shape

One type argument · adds dist_self, dist_comm, dist_triangle, edist, edist_dist, toUniformSpace, uniformity_dist, toBornology, cobounded_sets