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]
- to_has_dist : has_dist α
- dist_self : ∀ (x : α), has_dist.dist x x = 0
- dist_comm : ∀ (x y : α), has_dist.dist x y = has_dist.dist y x
- dist_triangle : ∀ (x y z : α), has_dist.dist x z ≤ has_dist.dist x y + has_dist.dist y z
The canonical equivalence relation on a premetric space.
Equations
- premetric.dist_setoid α = {r := λ (x y : α), has_dist.dist x y = 0, iseqv := _}
The canonical quotient of a premetric space, identifying points at distance 0.
Equations
@[instance]
Equations
- premetric.has_dist_metric_quot = {dist := quotient.lift₂ (λ (p q : α), has_dist.dist p q) premetric.has_dist_metric_quot._proof_1}
theorem
premetric.metric_quot_dist_eq
{α : Type u}
[premetric_space α]
(p q : α) :
has_dist.dist ⟦p⟧ ⟦q⟧ = has_dist.dist p q
@[instance]
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 : α), has_dist.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 : α), has_dist.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 := _}