Metric.NonemptyCompacts.dist_eq
theorem Metric.NonemptyCompacts.dist_eq :
∀ {α : Type u} [inst : MetricSpace α] {x y : TopologicalSpace.NonemptyCompacts α},
dist x y = Metric.hausdorffDist ↑x ↑y
The theorem states that for any metric space `α` and any two nonempty compact subspaces `x` and `y` of the topological space formed from `α`, the distance between `x` and `y` is equal to the Hausdorff distance between the sets underlying `x` and `y`. The Hausdorff distance, in this context, is the smallest non-negative real number `r` such that each set is included in the `r`-neighborhood of the other, or `0` if no such `r` exists.
More concisely: For any metric space `α` and compact subsets `x` and `y` of `α`, the metric distance between `x` and `y` equals the Hausdorff distance between `x` and `y`.
|
EMetric.Closeds.edist_eq
theorem EMetric.Closeds.edist_eq :
∀ {α : Type u} [inst : EMetricSpace α] {s t : TopologicalSpace.Closeds α},
edist s t = EMetric.hausdorffEdist ↑s ↑t
This theorem states that, for any two closed topological spaces `s` and `t` in any Emetric space `α`, the edistance (extended distance) between `s` and `t` is equal to the Hausdorff edistance of the corresponding sets. The Hausdorff edistance is defined as the smallest `r` such that each set is contained in the `r`-neighborhood of the other one. So in essence, this theorem is establishing a relationship between the edistance in a topological space and the Hausdorff edistance.
More concisely: In any metric space, the extended distance between two closed sets is equal to the Hausdorff distance between them.
|
EMetric.isClosed_subsets_of_isClosed
theorem EMetric.isClosed_subsets_of_isClosed :
∀ {α : Type u} [inst : EMetricSpace α] {s : Set α}, IsClosed s → IsClosed {t | ↑t ⊆ s}
This theorem states that for any type `α` equipped with an Emetric space structure, if `s` is a closed subset of `α`, then the collection of all subsets of `s` also forms a closed set. In mathematical terms, if `s` is a closed set in the Emetric space `α`, then the set `{t | t ⊆ s}` is also closed. Here, `{t | t ⊆ s}` denotes the set of all subsets `t` of `s`.
More concisely: If `α` is an Emetric space and `s` is a closed subset of `α`, then the set of all subsets of `s` is also closed.
|
EMetric.continuous_infEdist_hausdorffEdist
theorem EMetric.continuous_infEdist_hausdorffEdist :
∀ {α : Type u} [inst : EMetricSpace α], Continuous fun p => EMetric.infEdist p.1 ↑p.2
The theorem `EMetric.continuous_infEdist_hausdorffEdist` states that for any type `α` that is an instance of `EMetricSpace`, the function that maps a pair `p` (consisting of a point and a set) to the minimum extended distance (`infEdist`) of the point `p.1` to the set `p.2` is continuous. In other words, in any extended metric space, the minimal extended distance from a given point to a set varies continuously with the point and the set.
More concisely: The function that maps a point-set pair in an extended metric space to the minimum extended distance between them is continuous.
|
EMetric.NonemptyCompacts.isClosed_in_closeds
theorem EMetric.NonemptyCompacts.isClosed_in_closeds :
∀ {α : Type u} [inst : EMetricSpace α] [inst_1 : CompleteSpace α],
IsClosed (Set.range TopologicalSpace.NonemptyCompacts.toCloseds)
The theorem `EMetric.NonemptyCompacts.isClosed_in_closeds` states that for any type `α` that is equipped with an eMetricSpace structure and a CompleteSpace structure, the range of the function `TopologicalSpace.NonemptyCompacts.toCloseds` is a closed set. In other words, in a complete eMetric space, the set of all closed subsets that contain at least one point and are compact is itself a closed set.
More concisely: In a complete eMetric space, the set of all compact subsets containing at least one point is closed.
|
EMetric.NonemptyCompacts.ToCloseds.uniformEmbedding
theorem EMetric.NonemptyCompacts.ToCloseds.uniformEmbedding :
∀ {α : Type u} [inst : EMetricSpace α], UniformEmbedding TopologicalSpace.NonemptyCompacts.toCloseds
The theorem `EMetric.NonemptyCompacts.ToCloseds.uniformEmbedding` states that for any extended metric space `α`, the function `TopologicalSpace.NonemptyCompacts.toCloseds`, which translates nonempty compact subsets of `α` to closed subsets of `α`, is a uniform embedding. In other words, this function preserves the uniform (or topological) structure of the space, keeping distances between sets the same in the new representation as closed sets.
More concisely: The `TopologicalSpace.NonemptyCompacts.toCloseds` function, which maps nonempty compact subsets of an extended metric space to closed subsets, is a uniform embedding, preserving distances between sets.
|