Theorems · Inductive type · general topology

EMetricSpace

Type u → Type u

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].

Defined in

Mathlib.Topology.EMetricSpace.Defs

Cited by

242 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms