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_has_edist := {edist := λ (s t : topological_space.closeds α), emetric.Hausdorff_edist s.val t.val}, edist_self := _, eq_of_edist_eq_zero := _, edist_comm := _, edist_triangle := _, to_uniform_space := uniform_space_of_edist (λ (s t : topological_space.closeds α), emetric.Hausdorff_edist s.val t.val) emetric.closeds.emetric_space._proof_5 emetric.closeds.emetric_space._proof_6 emetric.closeds.emetric_space._proof_7, uniformity_edist := _}
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.
Equations
In a compact space, the type of closed subsets is compact.
Equations
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_has_edist := {edist := λ (s t : topological_space.nonempty_compacts α), emetric.Hausdorff_edist s.val t.val}, edist_self := _, eq_of_edist_eq_zero := _, edist_comm := _, edist_triangle := _, to_uniform_space := uniform_space_of_edist (λ (s t : topological_space.nonempty_compacts α), emetric.Hausdorff_edist s.val t.val) emetric.nonempty_compacts.emetric_space._proof_5 emetric.nonempty_compacts.emetric_space._proof_6 emetric.nonempty_compacts.emetric_space._proof_7, uniformity_edist := _}
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
Equations
In a compact space, the type of nonempty compact subsets is compact. This follows from the same statement for closed subsets
Equations
In a second countable space, the type of nonempty compact subsets is second countable
Equations
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