Theorems · Inductive type · general topology

PseudoMetricSpace

Type u → Type u

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

Cited by

1,550 results in Mathlib

Foundations

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