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 nonempty_compacts
) 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
Equations
- emetric.closeds.emetric_space = {to_pseudo_emetric_space := {to_has_edist := {edist := λ (s t : topological_space.closeds α), emetric.Hausdorff_edist ↑s ↑t}, edist_self := _, edist_comm := _, edist_triangle := _, to_uniform_space := uniform_space_of_edist (λ (s t : topological_space.closeds α), emetric.Hausdorff_edist ↑s ↑t) emetric.closeds.emetric_space._proof_4 emetric.closeds.emetric_space._proof_5 emetric.closeds.emetric_space._proof_6, uniformity_edist := _}, eq_of_edist_eq_zero := _}
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
Equations
- emetric.nonempty_compacts.emetric_space = {to_pseudo_emetric_space := {to_has_edist := {edist := λ (s t : topological_space.nonempty_compacts α), emetric.Hausdorff_edist ↑s ↑t}, edist_self := _, edist_comm := _, edist_triangle := _, to_uniform_space := uniform_space_of_edist (λ (s t : topological_space.nonempty_compacts α), emetric.Hausdorff_edist ↑s ↑t) emetric.nonempty_compacts.emetric_space._proof_4 emetric.nonempty_compacts.emetric_space._proof_5 emetric.nonempty_compacts.emetric_space._proof_6, uniformity_edist := _}, eq_of_edist_eq_zero := _}
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.
Equations
- metric.nonempty_compacts.metric_space = emetric_space.to_metric_space metric.nonempty_compacts.metric_space._proof_1
The distance on nonempty_compacts α
is the Hausdorff distance, by construction