# mathlibdocumentation

topology.metric_space.premetric_space

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

@[class]
structure premetric_space (α : Type u) :
Type u
• to_has_dist :
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z

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

def premetric.dist_setoid (α : Type u)  :

The canonical equivalence relation on a premetric space.

Equations
def premetric.metric_quot (α : Type u)  :
Type u

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

Equations
@[instance]
def premetric.has_dist_metric_quot {α : Type u}  :

Equations
theorem premetric.metric_quot_dist_eq {α : Type u} (p q : α) :
q = dist p q

@[instance]
def premetric.metric_space_quot {α : Type u}  :

Equations