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 NonemptyCompacts) also inherits a metric space structure from the Hausdorff distance, as the Hausdorff edistance is always finite in this context.

instance EMetric.Closeds.emetricSpace {α : Type u} [EMetricSpace α] : EMetricSpace (TopologicalSpace.Closeds α)

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

Equations

• EMetric.Closeds.emetricSpace = EMetricSpace.mk ⋯

theorem EMetric.continuous_infEdist_hausdorffEdist {α : Type u} [EMetricSpace α] : Continuous fun (p : α × TopologicalSpace.Closeds α) => EMetric.infEdist p.1 ↑p.2

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

theorem EMetric.isClosed_subsets_of_isClosed {α : Type u} [EMetricSpace α] {s : Set α} (hs : IsClosed s) : IsClosed {t : TopologicalSpace.Closeds α | ↑t ⊆ s}

Subsets of a given closed subset form a closed set

theorem EMetric.Closeds.edist_eq {α : Type u} [EMetricSpace α] {s : TopologicalSpace.Closeds α} {t : TopologicalSpace.Closeds α} : edist s t = EMetric.hausdorffEdist ↑s ↑t

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

instance EMetric.Closeds.completeSpace {α : Type u} [EMetricSpace α] [CompleteSpace α] : CompleteSpace (TopologicalSpace.Closeds α)

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

Equations

• ⋯ = ⋯

instance EMetric.Closeds.compactSpace {α : Type u} [EMetricSpace α] [CompactSpace α] : CompactSpace (TopologicalSpace.Closeds α)

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

Equations

• ⋯ = ⋯

instance EMetric.NonemptyCompacts.emetricSpace {α : Type u} [EMetricSpace α] : EMetricSpace (TopologicalSpace.NonemptyCompacts α)

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

Equations

• EMetric.NonemptyCompacts.emetricSpace = EMetricSpace.mk ⋯

theorem EMetric.NonemptyCompacts.ToCloseds.uniformEmbedding {α : Type u} [EMetricSpace α] : UniformEmbedding TopologicalSpace.NonemptyCompacts.toCloseds

NonemptyCompacts.toCloseds is a uniform embedding (as it is an isometry)

theorem EMetric.NonemptyCompacts.isClosed_in_closeds {α : Type u} [EMetricSpace α] [CompleteSpace α] : IsClosed (Set.range TopologicalSpace.NonemptyCompacts.toCloseds)

The range of NonemptyCompacts.toCloseds is closed in a complete space

instance EMetric.NonemptyCompacts.completeSpace {α : Type u} [EMetricSpace α] [CompleteSpace α] : CompleteSpace (TopologicalSpace.NonemptyCompacts α)

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

Equations

• ⋯ = ⋯

instance EMetric.NonemptyCompacts.compactSpace {α : Type u} [EMetricSpace α] [CompactSpace α] : CompactSpace (TopologicalSpace.NonemptyCompacts α)

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

Equations

• ⋯ = ⋯

instance EMetric.NonemptyCompacts.secondCountableTopology {α : Type u} [EMetricSpace α] [SecondCountableTopology α] : SecondCountableTopology (TopologicalSpace.NonemptyCompacts α)

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

Equations

• ⋯ = ⋯

instance Metric.NonemptyCompacts.metricSpace {α : Type u} [MetricSpace α] : MetricSpace (TopologicalSpace.NonemptyCompacts α)

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

Equations

• Metric.NonemptyCompacts.metricSpace = EMetricSpace.toMetricSpace ⋯

theorem Metric.NonemptyCompacts.dist_eq {α : Type u} [MetricSpace α] {x : TopologicalSpace.NonemptyCompacts α} {y : TopologicalSpace.NonemptyCompacts α} : dist x y = Metric.hausdorffDist ↑x ↑y

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

theorem Metric.lipschitz_infDist_set {α : Type u} [MetricSpace α] (x : α) : LipschitzWith 1 fun (s : TopologicalSpace.NonemptyCompacts α) => Metric.infDist x ↑s

theorem Metric.lipschitz_infDist {α : Type u} [MetricSpace α] : LipschitzWith 2 fun (p : α × TopologicalSpace.NonemptyCompacts α) => Metric.infDist p.1 ↑p.2

theorem Metric.uniformContinuous_infDist_Hausdorff_dist {α : Type u} [MetricSpace α] : UniformContinuous fun (p : α × TopologicalSpace.NonemptyCompacts α) => Metric.infDist p.1 ↑p.2