Theorems · Inductive type · general topology

PseudoEMetricSpace

Type u → Type u

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

Cited by

1,536 results in Mathlib

Foundations

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