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.

theorem Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt {α : Type u_1} [PseudoEMetricSpace α] {s t : Set α} {δ : ENNReal} (h : hausdorffEDist s t < δ) : (s, t) ∈ hausdorffEntourage {p : α × α | edist p.1 p.2 < δ}

theorem Metric.hausdorffEDist_le_of_mem_hausdorffEntourage {α : Type u_1} [PseudoEMetricSpace α] {s t : Set α} {δ : ENNReal} (h : (s, t) ∈ hausdorffEntourage {p : α × α | edist p.1 p.2 ≤ δ}) : hausdorffEDist s t ≤ δ

@[reducible, inline]

abbrev PseudoEMetricSpace.hausdorff {α : Type u_1} [PseudoEMetricSpace α] : PseudoEMetricSpace (Set α)

The Hausdorff pseudo emetric on the powerset of a pseudo emetric space. See note [reducible non-instances].

instance TopologicalSpace.Closeds.instEMetricSpace {α : Type u_1} [EMetricSpace α] : EMetricSpace (Closeds α)

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

theorem TopologicalSpace.Closeds.continuous_infEDist {α : Type u_1} [EMetricSpace α] : Continuous fun (p : α × Closeds α) => Metric.infEDist p.1 ↑p.2

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

theorem TopologicalSpace.Closeds.edist_eq {α : Type u_1} [EMetricSpace α] {s t : Closeds α} : edist s t = Metric.hausdorffEDist ↑s ↑t

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

instance TopologicalSpace.Closeds.instCompleteSpace {α : Type u_1} [EMetricSpace α] [CompleteSpace α] : CompleteSpace (Closeds α)

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

theorem TopologicalSpace.Closeds.isometry_singleton {α : Type u_1} [EMetricSpace α] : Isometry fun (x : α) => {x}

theorem TopologicalSpace.Closeds.lipschitz_sup {α : Type u_1} [EMetricSpace α] : LipschitzWith 1 fun (p : Closeds α × Closeds α) => p.1 ⊔ p.2

instance TopologicalSpace.Compacts.instEMetricSpace {α : Type u_1} [EMetricSpace α] : EMetricSpace (Compacts α)

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

theorem TopologicalSpace.Compacts.edist_eq {α : Type u_1} [EMetricSpace α] {s t : Compacts α} : edist s t = Metric.hausdorffEDist ↑s ↑t

theorem TopologicalSpace.Compacts.isometry_toCloseds {α : Type u_1} [EMetricSpace α] : Isometry toCloseds

theorem TopologicalSpace.Compacts.isometry_singleton {α : Type u_1} [EMetricSpace α] : Isometry fun (x : α) => {x}

theorem TopologicalSpace.Compacts.lipschitz_sup {α : Type u_1} [EMetricSpace α] : LipschitzWith 1 fun (p : Compacts α × Compacts α) => p.1 ⊔ p.2

theorem TopologicalSpace.Compacts.lipschitz_prod {α : Type u_1} {β : Type u_2} [EMetricSpace α] [EMetricSpace β] : LipschitzWith 1 fun (p : Compacts α × Compacts β) => p.1 ×ˢ p.2

instance TopologicalSpace.NonemptyCompacts.instEMetricSpace {α : Type u_1} [EMetricSpace α] : EMetricSpace (NonemptyCompacts α)

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

theorem TopologicalSpace.NonemptyCompacts.isometry_toCloseds {α : Type u_1} [EMetricSpace α] : Isometry toCloseds

NonemptyCompacts.toCloseds is an isometry

theorem TopologicalSpace.NonemptyCompacts.isometry_toCompacts {α : Type u_1} [EMetricSpace α] : Isometry toCompacts

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

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

instance TopologicalSpace.NonemptyCompacts.instCompleteSpace {α : Type u_1} [EMetricSpace α] [CompleteSpace α] : CompleteSpace (NonemptyCompacts α)

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

instance TopologicalSpace.NonemptyCompacts.instSecondCountableTopology {α : Type u_1} [EMetricSpace α] [SecondCountableTopology α] : SecondCountableTopology (NonemptyCompacts α)

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

theorem TopologicalSpace.NonemptyCompacts.isometry_singleton {α : Type u_1} [EMetricSpace α] : Isometry fun (x : α) => {x}

theorem TopologicalSpace.NonemptyCompacts.lipschitz_sup {α : Type u_1} [EMetricSpace α] : LipschitzWith 1 fun (p : NonemptyCompacts α × NonemptyCompacts α) => p.1 ⊔ p.2

theorem TopologicalSpace.NonemptyCompacts.lipschitz_prod {α : Type u_1} {β : Type u_2} [EMetricSpace α] [EMetricSpace β] : LipschitzWith 1 fun (p : NonemptyCompacts α × NonemptyCompacts β) => p.1 ×ˢ p.2

@[deprecated TopologicalSpace.NonemptyCompacts.continuous_toCloseds (since := "2025-11-19")]

theorem EMetric.NonemptyCompacts.continuous_toCloseds {α : Type u_1} [UniformSpace α] [T2Space α] : Continuous TopologicalSpace.NonemptyCompacts.toCloseds

Alias of TopologicalSpace.NonemptyCompacts.continuous_toCloseds.

@[deprecated TopologicalSpace.Closeds.isClosed_subsets_of_isClosed (since := "2025-08-20")]

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

Alias of TopologicalSpace.Closeds.isClosed_subsets_of_isClosed.

@[deprecated TopologicalSpace.NonemptyCompacts.isClosed_subsets_of_isClosed (since := "2025-11-19")]

theorem EMetric.NonemptyCompacts.isClosed_subsets_of_isClosed {α : Type u_1} [TopologicalSpace α] {F : Set α} (h : IsClosed F) : IsClosed {K : TopologicalSpace.NonemptyCompacts α | ↑K ⊆ F}

Alias of TopologicalSpace.NonemptyCompacts.isClosed_subsets_of_isClosed.

@[deprecated TopologicalSpace.Closeds.isClosed_subsets_of_isClosed (since := "2025-11-19")]

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

Alias of TopologicalSpace.Closeds.isClosed_subsets_of_isClosed.

@[deprecated Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt (since := "2026-01-08")]

theorem EMetric.mem_hausdorffEntourage_of_hausdorffEdist_lt {α : Type u_1} [PseudoEMetricSpace α] {s t : Set α} {δ : ENNReal} (h : Metric.hausdorffEDist s t < δ) : (s, t) ∈ hausdorffEntourage {p : α × α | edist p.1 p.2 < δ}

Alias of Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt.

@[deprecated Metric.hausdorffEDist_le_of_mem_hausdorffEntourage (since := "2026-01-08")]

theorem EMetric.hausdorffEdist_le_of_mem_hausdorffEntourage {α : Type u_1} [PseudoEMetricSpace α] {s t : Set α} {δ : ENNReal} (h : (s, t) ∈ hausdorffEntourage {p : α × α | edist p.1 p.2 ≤ δ}) : Metric.hausdorffEDist s t ≤ δ

Alias of Metric.hausdorffEDist_le_of_mem_hausdorffEntourage.

@[deprecated TopologicalSpace.Closeds.continuous_infEDist (since := "2026-01-08")]

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

Alias of TopologicalSpace.Closeds.continuous_infEDist.

---

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

@[deprecated TopologicalSpace.Closeds.edist_eq (since := "2026-01-08")]

theorem EMetric.Closeds.edist_eq {α : Type u_1} [EMetricSpace α] {s t : TopologicalSpace.Closeds α} : edist s t = Metric.hausdorffEDist ↑s ↑t

Alias of TopologicalSpace.Closeds.edist_eq.

---

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

@[deprecated TopologicalSpace.Closeds.isometry_singleton (since := "2026-01-08")]

theorem EMetric.Closeds.isometry_singleton {α : Type u_1} [EMetricSpace α] : Isometry fun (x : α) => {x}

Alias of TopologicalSpace.Closeds.isometry_singleton.

@[deprecated TopologicalSpace.Closeds.lipschitz_sup (since := "2026-01-08")]

theorem EMetric.Closeds.lipschitz_sup {α : Type u_1} [EMetricSpace α] : LipschitzWith 1 fun (p : TopologicalSpace.Closeds α × TopologicalSpace.Closeds α) => p.1 ⊔ p.2

Alias of TopologicalSpace.Closeds.lipschitz_sup.

@[deprecated TopologicalSpace.NonemptyCompacts.isometry_toCloseds (since := "2026-01-08")]

theorem EMetric.NonemptyCompacts.isometry_toCloseds {α : Type u_1} [EMetricSpace α] : Isometry TopologicalSpace.NonemptyCompacts.toCloseds

Alias of TopologicalSpace.NonemptyCompacts.isometry_toCloseds.

---

NonemptyCompacts.toCloseds is an isometry

@[deprecated TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds (since := "2025-08-20")]

theorem EMetric.NonemptyCompacts.ToCloseds.isUniformEmbedding {α : Type u_1} [UniformSpace α] [T2Space α] : IsUniformEmbedding TopologicalSpace.NonemptyCompacts.toCloseds

Alias of TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds.

@[deprecated TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds (since := "2025-11-19")]

theorem EMetric.NonemptyCompacts.isUniformEmbedding_toCloseds {α : Type u_1} [UniformSpace α] [T2Space α] : IsUniformEmbedding TopologicalSpace.NonemptyCompacts.toCloseds

Alias of TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds.

@[deprecated TopologicalSpace.NonemptyCompacts.isClosed_in_closeds (since := "2026-01-08")]

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

Alias of TopologicalSpace.NonemptyCompacts.isClosed_in_closeds.

---

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

@[deprecated TopologicalSpace.NonemptyCompacts.isometry_singleton (since := "2026-01-08")]

theorem EMetric.NonemptyCompacts.isometry_singleton {α : Type u_1} [EMetricSpace α] : Isometry fun (x : α) => {x}

Alias of TopologicalSpace.NonemptyCompacts.isometry_singleton.

@[deprecated TopologicalSpace.NonemptyCompacts.lipschitz_sup (since := "2026-01-08")]

theorem EMetric.NonemptyCompacts.lipschitz_sup {α : Type u_1} [EMetricSpace α] : LipschitzWith 1 fun (p : TopologicalSpace.NonemptyCompacts α × TopologicalSpace.NonemptyCompacts α) => p.1 ⊔ p.2

Alias of TopologicalSpace.NonemptyCompacts.lipschitz_sup.

@[deprecated TopologicalSpace.NonemptyCompacts.lipschitz_prod (since := "2026-01-08")]

theorem EMetric.NonemptyCompacts.lipschitz_prod {α : Type u_1} {β : Type u_2} [EMetricSpace α] [EMetricSpace β] : LipschitzWith 1 fun (p : TopologicalSpace.NonemptyCompacts α × TopologicalSpace.NonemptyCompacts β) => p.1 ×ˢ p.2

Alias of TopologicalSpace.NonemptyCompacts.lipschitz_prod.

instance Metric.NonemptyCompacts.instMetricSpace {α : Type u_1} [MetricSpace α] : MetricSpace (TopologicalSpace.NonemptyCompacts α)

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

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

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

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

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

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