mathlib3 documentation

topology.metric_space.closeds

Closed subsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[protected, instance]
noncomputable def emetric.closeds.emetric_space {α : Type u} [emetric_space α] :
emetric_space (topological_space.closeds α)

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

Equations
source
theorem emetric.continuous_inf_edist_Hausdorff_edist {α : Type u} [emetric_space α] :
continuous (λ (p : α × topological_space.closeds α), emetric.inf_edist p.fst ↑(p.snd))

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

source
theorem emetric.is_closed_subsets_of_is_closed {α : Type u} [emetric_space α] {s : set α} (hs : is_closed s) :
is_closed {t : topological_space.closeds α | ↑t ⊆ s}

Subsets of a given closed subset form a closed set

source
theorem emetric.closeds.edist_eq {α : Type u} [emetric_space α] {s t : topological_space.closeds α} :
has_edist.edist s t = emetric.Hausdorff_edist ↑s ↑t

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

source
@[protected, instance]
def emetric.closeds.complete_space {α : Type u} [emetric_space α] [complete_space α] :
complete_space (topological_space.closeds α)

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

source
@[protected, instance]
def emetric.closeds.compact_space {α : Type u} [emetric_space α] [compact_space α] :
compact_space (topological_space.closeds α)

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

source
@[protected, instance]
noncomputable def emetric.nonempty_compacts.emetric_space {α : Type u} [emetric_space α] :
emetric_space (topological_space.nonempty_compacts α)

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

Equations
source
theorem emetric.nonempty_compacts.to_closeds.uniform_embedding {α : Type u} [emetric_space α] :
uniform_embedding topological_space.nonempty_compacts.to_closeds

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

source
theorem emetric.nonempty_compacts.is_closed_in_closeds {α : Type u} [emetric_space α] [complete_space α] :
is_closed (set.range topological_space.nonempty_compacts.to_closeds)

The range of nonempty_compacts.to_closeds is closed in a complete space

source
@[protected, instance]
def emetric.nonempty_compacts.complete_space {α : Type u} [emetric_space α] [complete_space α] :
complete_space (topological_space.nonempty_compacts α)

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

source
@[protected, instance]
def emetric.nonempty_compacts.compact_space {α : Type u} [emetric_space α] [compact_space α] :
compact_space (topological_space.nonempty_compacts α)

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

source
@[protected, instance]
def emetric.nonempty_compacts.second_countable_topology {α : Type u} [emetric_space α] [topological_space.second_countable_topology α] :
topological_space.second_countable_topology (topological_space.nonempty_compacts α)

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

source
@[protected, instance]
noncomputable def metric.nonempty_compacts.metric_space {α : Type u} [metric_space α] :
metric_space (topological_space.nonempty_compacts α)

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

Equations
source
theorem metric.nonempty_compacts.dist_eq {α : Type u} [metric_space α] {x y : topological_space.nonempty_compacts α} :
has_dist.dist x y = metric.Hausdorff_dist ↑x ↑y

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

source
theorem metric.lipschitz_inf_dist_set {α : Type u} [metric_space α] (x : α) :
lipschitz_with 1 (λ (s : topological_space.nonempty_compacts α), metric.inf_dist x ↑s)
source
theorem metric.lipschitz_inf_dist {α : Type u} [metric_space α] :
lipschitz_with 2 (λ (p : α × topological_space.nonempty_compacts α), metric.inf_dist p.fst ↑(p.snd))
source
theorem metric.uniform_continuous_inf_dist_Hausdorff_dist {α : Type u} [metric_space α] :
uniform_continuous (λ (p : α × topological_space.nonempty_compacts α), metric.inf_dist p.fst ↑(p.snd))