Closed subsets #
This file defines the metric and emetric space structure on the types of closed subsets and nonempty compact subsets of a metric or emetric space.
The Hausdorff distance induces an emetric space structure on the type of closed subsets
of an emetric space, called
Closeds. Its completeness, resp. compactness, resp.
second-countability, follow from the corresponding properties of the original space.
In a metric space, the type of nonempty compact subsets (called
inherits a metric space structure from the Hausdorff distance, as the Hausdorff edistance is
always finite in this context.
NonemptyCompacts.toCloseds is a uniform embedding (as it is an isometry)