# 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 `NonemptyCompacts`

) also
inherits a metric space structure from the Hausdorff distance, as the Hausdorff edistance is
always finite in this context.

In emetric spaces, the Hausdorff edistance defines an emetric space structure on the type of closed subsets

The edistance to a closed set depends continuously on the point and the set

Subsets of a given closed subset form a closed set

By definition, the edistance on `Closeds α`

is given by the Hausdorff edistance

In a complete space, the type of closed subsets is complete for the Hausdorff edistance.

In a compact space, the type of closed subsets is compact.

In an emetric space, the type of non-empty compact subsets is an emetric space, where the edistance is the Hausdorff edistance

`NonemptyCompacts.toCloseds`

is a uniform embedding (as it is an isometry)

The range of `NonemptyCompacts.toCloseds`

is closed in a complete space

In a complete space, the type of nonempty compact subsets is complete. This follows from the same statement for closed subsets

In a compact space, the type of nonempty compact subsets is compact. This follows from the same statement for closed subsets

In a second countable space, the type of nonempty compact subsets is second countable

`NonemptyCompacts α`

inherits a metric space structure, as the Hausdorff
edistance between two such sets is finite.

The distance on `NonemptyCompacts α`

is the Hausdorff distance, by construction