ms-0.2.1: metric spaces
A MetricSpace
is a set together with a notion of distance between
elements. Distance is computed by a function dist
which has the following
four laws:
- non-negative:
forall x y.
dist
x y >= 0 - identity of indiscernibles:
forall x y.
dist
x y == 0 <=> x == y - symmetry:
forall x y. dist x y ==
dist
y x - triangle inequality:
forall x y z.
dist
x z <=dist
x y +dist
y z
See the Wikipedia article on metric spaces for more details.
- Math