mathlib documentation


Premetric spaces

Metric spaces are often defined as quotients of spaces endowed with a "distance" function satisfying the triangular inequality, but for which dist x y = 0 does not imply x = y. We call such a space a premetric space. dist x y = 0 defines an equivalence relation, and the quotient is canonically a metric space.

structure premetric_space  :
Type uType u

theorem premetric.dist_nonneg {α : Type u} [premetric_space α] {x y : α} :
0 dist x y

def premetric.dist_setoid (α : Type u) [premetric_space α] :

The canonical equivalence relation on a premetric space.

def premetric.metric_quot (α : Type u) [premetric_space α] :
Type u

The canonical quotient of a premetric space, identifying points at distance 0.


theorem premetric.metric_quot_dist_eq {α : Type u} [premetric_space α] (p q : α) :