mathlib documentation

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 : 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} [premetric_space α] {x y : α} :

0 ≤ dist x y

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

The canonical equivalence relation on a premetric space.

Equations

premetric.dist_setoid α = {r := λ (x y : α), dist x y = 0, iseqv := _}

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

Type u

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

Equations

premetric.metric_quot α = quotient (premetric.dist_setoid α)

@[instance]

def premetric.has_dist_metric_quot {α : Type u} [premetric_space α] :

has_dist (premetric.metric_quot α)

Equations

premetric.has_dist_metric_quot = {dist := quotient.lift₂ (λ (p q : α), dist p q) premetric.has_dist_metric_quot._proof_1}

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

dist ⟦p⟧ ⟦q⟧ = dist p q

@[instance]

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

metric_space (premetric.metric_quot α)

Equations

premetric.metric_space_quot = {to_has_dist := premetric.has_dist_metric_quot _inst_1, dist_self := _, eq_of_dist_eq_zero := _, dist_comm := _, dist_triangle := _, edist := λ (x y : premetric.metric_quot α), ennreal.of_real (quotient.lift₂ (λ (p q : α), dist p q) premetric.has_dist_metric_quot._proof_1 x y), edist_dist := _, to_uniform_space := uniform_space_of_dist (quotient.lift₂ (λ (p q : α), dist p q) premetric.has_dist_metric_quot._proof_1) premetric.metric_space_quot._proof_6 premetric.metric_space_quot._proof_7 premetric.metric_space_quot._proof_8, uniformity_dist := _}