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

nonempty_compacts.to_closeds is a uniform embedding (as it is an isometry)

The range of nonempty_compacts.to_closeds 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

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

The distance on nonempty_compacts α is the Hausdorff distance, by construction