Skip to main content

MetricSpace

typeclass M: MetricSpace {
    distance: (M, M) -> Real
    self_distance_is_zero(x: M) {
        x.distance(x) = 0
    }
    dist_zero_imp_eq(x: M, y: M) {
        x.distance(y) = 0 implies x = y
    }
    symmetric(x: M, y: M) {
        x.distance(y) = y.distance(x)
    }
    triangle(x: M, y: M, z: M) {
        x.distance(z) <= x.distance(y) + y.distance(z)
    }
}

A metric space is a set equipped with a distance function that satisfies specific axioms. The distance function must be non-negative, symmetric, and satisfy the triangle inequality.

GitHub

dist_zero_imp_eq​

dist_zero_imp_eq(x: M, y: M) {
    x.distance(y) = 0 implies x = y
}

Rule: distance zero means the points are equal

distance​

distance: (M, M) -> Real

Every metric space must have a distance function

self_distance_is_zero​

self_distance_is_zero(x: M) {
    x.distance(x) = 0
}

Rule: the distance from a point to itself is zero

symmetric​

symmetric(x: M, y: M) {
    x.distance(y) = y.distance(x)
}

Rule: distance must be symmetric

triangle​

triangle(x: M, y: M, z: M) {
    x.distance(z) <= x.distance(y) + y.distance(z)
}

Rule: distance must satisfy the triangle inequality