Theorems · Inductive type · general topology

MetricSpace

Type u → Type u

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

Defined in

Mathlib.Topology.MetricSpace.Defs

Cited by

1,684 results in Mathlib

Foundations

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