mathlib documentation

topology.metric_space.closeds

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.

@[instance]

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

Equations

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

theorem emetric.is_closed_subsets_of_is_closed {α : Type u} [emetric_space α] {s : set α} :

Subsets of a given closed subset form a closed set

By definition, the edistance on closeds α is given by the Hausdorff edistance

@[instance]

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

@[instance]

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

@[instance]

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

Equations

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

@[instance]

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

@[instance]

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

@[instance]

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

@[instance]

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

Equations

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