Metric Spaces

Description: This library formalizes metric spaces. This unique formulation defines a metric as a ball relation ball : Qpos -> X -> X -> Prop.
The formalization includes:

definition of metrics and uniformly continuous functions
product metrics
a monadic completion operation for creating complete metric spaces
a compact operation for creating the metric space of compact subsets of metric spaces using the Hausdorff metric
a metric space of step functions.

References:

Russell O’Connor. "A monadic, functional implementation of real numbers", Mathematical. Structures in Comp. Sci., 17(1):129–159, 2007.
Russell O’Connor. "Certified exact transcendental real number computation in Coq". In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, LNCS. Springer-Verlag, 2008. to appear.
Russell O’Connor. "A Computer Verified Theory of Compact Sets". to appear.

Maintainer: Russell O’Connor

Developers: Russell O’Connor