EMetric.infEdist_le_hausdorffEdist_of_mem
theorem EMetric.infEdist_le_hausdorffEdist_of_mem :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α},
x ∈ s → EMetric.infEdist x t ≤ EMetric.hausdorffEdist s t
This theorem, titled "The distance to a set is controlled by the Hausdorff distance", states that for any type `α` that is a pseudo extended metric space, given any two sets `s` and `t` of type `α` and an element `x` of type `α` that belongs to set `s`, the minimal extended distance from `x` to set `t` is less than or equal to the Hausdorff extended distance between the two sets `s` and `t`. In other words, the least distance from a point to a set of elements in a pseudo extended metric space is always bounded above by the Hausdorff distance between the set containing the point and the other set.
More concisely: For any pseudo extended metric space `α`, and sets `s` and `t` in `α` with `x` in `s`, the minimal extended distance from `x` to `t` is bounded above by the Hausdorff extended distance between `s` and `t`.
|
Metric.hausdorffDist_le_of_infDist
theorem Metric.hausdorffDist_le_of_infDist :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {r : ℝ},
0 ≤ r → (∀ x ∈ s, Metric.infDist x t ≤ r) → (∀ x ∈ t, Metric.infDist x s ≤ r) → Metric.hausdorffDist s t ≤ r
This theorem states that for any two sets, `s` and `t`, of type `α` in a pseudo-metric space, and a nonnegative real number `r`, if the minimal distance from any point in `s` to `t` and from any point in `t` to `s` is less than or equal to `r`, then the Hausdorff distance between `s` and `t` is also less than or equal to `r`. The Hausdorff distance is a measure of the greatest of all the distances from a point in one set to the closest point in the other set.
More concisely: In a pseudo-metric space, if the smallest distance between any point in sets `s` and `t` of type `α` exceeds their Hausdorff distance by a nonnegative real number `r`, then `r` is an upper bound for the Hausdorff distance between `s` and `t`.
|
Metric.infDist_lt_iff
theorem Metric.infDist_lt_iff :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α} {r : ℝ},
s.Nonempty → (Metric.infDist x s < r ↔ ∃ y ∈ s, dist x y < r)
This theorem states that in any pseudo metric space, the minimal distance from a point 'x' to a set 's' is less than a real number 'r' if and only if there exists a point 'y' in the set 's' such that the distance from 'x' to 'y' is less than 'r'. This theorem assumes that the set 's' is not empty. In other words, it is connecting the concept of the infimum distance between a point and a set with the existence of a specific point in that set satisfying a certain distance condition.
More concisely: In a pseudo metric space, the point 'x' has distance less than 'r' to set 's' if and only if there exists a point 'y' in 's' with distance from 'x' to 'y' < 'r'.
|
Metric.hausdorffDist_self_zero
theorem Metric.hausdorffDist_self_zero :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Metric.hausdorffDist s s = 0
This theorem states that in a pseudometric space, the Hausdorff distance between any set and itself is always zero. The Hausdorff distance is a measure of the greatest of all distances from a point in one set to the closest point in the other set. In this case, since we are comparing a set to itself, the distance between any point and its closest neighbor in the same set is trivially zero, which makes the Hausdorff distance also zero.
More concisely: In a pseudometric space, the Hausdorff distance between a set and itself is equal to zero.
|
Metric.hausdorffDist_closure₂
theorem Metric.hausdorffDist_closure₂ :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
Metric.hausdorffDist s (closure t) = Metric.hausdorffDist s t
This theorem states that for any two sets `s` and `t` in a pseudometric space `α`, taking the closure of the set `t` does not change the Hausdorff distance between set `s` and set `t`. In other words, the Hausdorff distance from `s` to `t` is identical to the Hausdorff distance from `s` to the closure of `t`. The Hausdorff distance, in this context, is the smallest nonnegative real number such that each set is included in the respective neighborhood of the other. The closure of a set is the smallest closed set containing the original set.
More concisely: The Hausdorff distance between a set `s` and a set `t` in a pseudometric space equals the Hausdorff distance between `s` and the closure of `t`.
|
Metric.uniformContinuous_infDist_pt
theorem Metric.uniformContinuous_infDist_pt :
∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), UniformContinuous fun x => Metric.infDist x s
This theorem states that, given any set `s` in a pseudometric space `α`, the function that maps each point `x` in `α` to its minimal distance to the set `s` is uniformly continuous. In other words, for any two points close to each other in `α`, their minimal distances to the set `s` are also close, regardless of where the two points are located in `α`. This concept is an important part in the theory of metric and topological spaces, and is fundamental in mathematical analysis.
More concisely: Given any subset `s` of a pseudometric space `α`, the function mapping each point `x` to the distance `d(x, s)` is uniformly continuous.
|
Metric.hausdorffDist_empty
theorem Metric.hausdorffDist_empty :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Metric.hausdorffDist s ∅ = 0
The theorem `Metric.hausdorffDist_empty` states that for any set `s` in a pseudometric space `α`, the Hausdorff distance between the set `s` and the empty set is zero. The Hausdorff distance is a measure of how far two subsets of a metric space are from each other. In this case, if one of the sets is the empty set, the distance is defined to be zero. Note that this theorem uses the real-valued version of the Hausdorff distance (`Metric.hausdorffDist`), not the extended real-valued version (`EMetric.hausdorffEdist`), which would yield a value of `∞` for the Hausdorff distance to the empty set.
More concisely: The Hausdorff distance between a set and the empty set in a pseudometric space is zero.
|
EMetric.hausdorffEdist_self
theorem EMetric.hausdorffEdist_self :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, EMetric.hausdorffEdist s s = 0
This theorem states that the Hausdorff edistance (extended metric) of a set to itself is always zero. In other words, for any set `s` in a given pseudo extended metric space `α`, if you calculate the Hausdorff edistance from the set `s` to the same set `s`, the result will always be zero. This is consistent with the general principle that the distance from any point to itself, in any conventional metric space, is zero.
More concisely: In any pseudo extended metric space, the Hausdorff distance between a set and itself is zero.
|
EMetric.infEdist_anti
theorem EMetric.infEdist_anti :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α},
s ⊆ t → EMetric.infEdist x t ≤ EMetric.infEdist x s
The theorem `EMetric.infEdist_anti` states that for any type `α` equipped with a `PseudoEMetricSpace` structure, and given any point `x` of type `α` and any two sets `s` and `t` of type `α`, if `s` is a subset of `t`, then the infimum extended distance from `x` to `t` is less than or equal to the infimum extended distance from `x` to `s`. In other words, the minimal extended distance from a point to a set is anti-monotonic with respect to the inclusion of the set.
More concisely: For any pseudo-metric space `(α, d)`, and point `x ∈ α`, if `s ⊆ t` are subsets of `α`, then `inf (d x i : i ∈ s) ≤ inf (d x j : j ∈ t)`.
|
EMetric.hausdorffEdist_closure₂
theorem EMetric.hausdorffEdist_closure₂ :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
EMetric.hausdorffEdist s (closure t) = EMetric.hausdorffEdist s t
This theorem states that for any given pseudoemetric space `α` and any two sets `s` and `t` of `α`, the Hausdorff extended metric or edistance between the set `s` and the closure of the set `t` is the same as that between `s` and `t` itself. In other words, closing the set `t` does not change the Hausdorff edistance to `s`. Here, the closure of a set refers to the smallest closed set that contains the set, and the Hausdorff edistance refers to the smallest non-negative real number `r` such that each point of each set is not farther than `r` from some point of the other set.
More concisely: The Hausdorff extended metric between a set and its closure is equal to the Hausdorff extended metric between the set and the original set.
|
Metric.lipschitz_infNndist_pt
theorem Metric.lipschitz_infNndist_pt :
∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), LipschitzWith 1 fun x => Metric.infNndist x s
The theorem `Metric.lipschitz_infNndist_pt` states that, for any given set `s` in a pseudo-metric space (denoted by `α`), the function that maps each point `x` in `α` to the minimal distance from `x` to the set `s` is Lipschitz continuous with a Lipschitz constant of 1. In mathematical terms, for all points `x` and `y` in `α`, the difference in the minimal distances of `x` and `y` to the set `s` is less than or equal to the distance between `x` and `y`.
More concisely: The function that maps each point in a pseudo-metric space to the minimal distance from that point to a given set is Lipschitz continuous with a constant of 1.
|
EMetric.hausdorffEdist_le_of_mem_edist
theorem EMetric.hausdorffEdist_le_of_mem_edist :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α} {r : ENNReal},
(∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r) → (∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r) → EMetric.hausdorffEdist s t ≤ r
This theorem states that given any two sets `s` and `t` in a pseudo extended metric space `α`, and a nonnegative extended real number `r`, if for every element `x` in `s` there exists an element `y` in `t` such that the extended distance between `x` and `y` is less than or equal to `r`, and for every element `x` in `t` there exists an element `y` in `s` such that the extended distance between `x` and `y` is less than or equal to `r`, then the Hausdorff extended distance between the sets `s` and `t` is less than or equal to `r`. In other words, the Hausdorff extended distance between two sets can be bounded by showing that for any point in each set, there's a point in the other set at a controlled distance.
More concisely: Given two sets in a pseudo extended metric space, if for every element in each set there exists an element in the other set with extended distance less than or equal to a given nonnegative extended real number, then the Hausdorff extended distance between the sets is less than or equal to that number.
|
Metric.hausdorffDist_self_closure
theorem Metric.hausdorffDist_self_closure :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Metric.hausdorffDist s (closure s) = 0
The theorem `Metric.hausdorffDist_self_closure` states that for any set `s` in a space `α` (where `α` is a pseudo-metric space), the Hausdorff distance between the set `s` and its closure is zero. In other words, given a set within a space that follows the rules of a pseudo-metric space, the smallest nonnegative distance (`r`) such that each element of the set and its closure (the smallest closed set containing `s`) are within `r` of each other is always zero.
More concisely: The Hausdorff distance between a set and its closure in a pseudo-metric space is zero.
|
EMetric.infEdist_pos_iff_not_mem_closure
theorem EMetric.infEdist_pos_iff_not_mem_closure :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {E : Set α}, 0 < EMetric.infEdist x E ↔ x ∉ closure E := by
sorry
The theorem `EMetric.infEdist_pos_iff_not_mem_closure` states that for any type `α` that has a `PseudoEMetricSpace` structure, a point `x` of this type, and a set `E` of this type, the infimum extended distance (or the smallest possible extended distance) from the point `x` to the set `E` is greater than zero if and only if the point `x` is not in the closure of the set `E`. The closure of a set is the smallest closed set containing the set. In this context, the extended distance can be thought of as a generalized distance that can take on the value of infinity, which is useful for handling certain mathematical cases.
More concisely: For any `PseudoEMetricSpace` `α`, point `x` in `α`, and set `E` in `α`, the infimum of extended distances from `x` to `E` is positive if and only if `x` is not in the closure of `E`.
|
EMetric.hausdorffEdist_closure
theorem EMetric.hausdorffEdist_closure :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
EMetric.hausdorffEdist (closure s) (closure t) = EMetric.hausdorffEdist s t
The theorem `EMetric.hausdorffEdist_closure` states that for any pair of sets `s` and `t` within a type `α` that forms a pseudo emetric space, the Hausdorff edistance (the minimal radius needed such that each set lies within the neighborhood of the other) between the closure of `s` and the closure of `t` is exactly the same as the Hausdorff edistance between `s` and `t` originally. In other words, the process of taking the closure of the sets, which involves including all limit points, doesn't change the Hausdorff edistance between the two sets.
More concisely: The Hausdorff distance between the closures of two sets in a pseudo metric space equals the Hausdorff distance between the original sets.
|
EMetric.infEdist_le_infEdist_add_edist
theorem EMetric.infEdist_le_infEdist_add_edist :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s : Set α},
EMetric.infEdist x s ≤ EMetric.infEdist y s + edist x y
This theorem states that for any pseudo extended metric space and for any two points `x` and `y` within this space, as well as any set `s` of points in the same space, the minimum extended distance from `x` to `s` is less than or equal to the sum of the minimum extended distance from `y` to `s` and the extended distance from `x` to `y`. Here, the minimum extended distance from a point to a set is the infimum of the extended distances from the point to the elements of the set. This is a property of distances that is often used in geometric and topological proofs.
More concisely: For any pseudo extended metric space and points `x`, `y` within it, and set `s` of points in the same space, the minimum extended distance from `x` to `s` is less than or equal to the minimum extended distance from `y` to `s` plus the extended distance from `x` to `y`.
|
Metric.continuous_infDist_pt
theorem Metric.continuous_infDist_pt :
∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), Continuous fun x => Metric.infDist x s
This theorem states that for any set `s` in a given pseudometric space `α`, the function that calculates the minimum distance from a point `x` to the set `s` (denoted as `Metric.infDist x s`) is a continuous function. In other words, small changes in the point `x` result in small changes in the computed minimum distance. This applies to all pseudometric spaces, which are mathematical structures that generalize the concept of metric spaces by relaxing the requirement that the distance between distinct points must be positive.
More concisely: The function `Metric.infDist x : Set → Real` is continuous for any point `x` in a pseudometric space.
|
Metric.hausdorffDist_le_diam
theorem Metric.hausdorffDist_le_diam :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
s.Nonempty →
Bornology.IsBounded s → t.Nonempty → Bornology.IsBounded t → Metric.hausdorffDist s t ≤ Metric.diam (s ∪ t)
This theorem states that for any two nonempty and bounded sets `s` and `t` in a pseudo-metric space `α`, the Hausdorff distance between `s` and `t` is less than or equal to the diameter of the union of `s` and `t`. The Hausdorff distance is defined as the smallest nonnegative real number `r` such that each of the sets is included in the `r`-neighborhood of the other, while the diameter of a set is the greatest distance between any two points in the set. If there is no such `r`, the Hausdorff distance is defined to be `0`. The notion of a set being bounded is relative to the ambient bornology on `α`.
More concisely: For any two nonempty, bounded sets `s` and `t` in a pseudometric space `α`, the Hausdorff distance between `s` and `t` is less than or equal to the diameter of their union.
|
Metric.hausdorffDist_image
theorem Metric.hausdorffDist_image :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {s t : Set α} {Φ : α → β},
Isometry Φ → Metric.hausdorffDist (Φ '' s) (Φ '' t) = Metric.hausdorffDist s t
The theorem `Metric.hausdorffDist_image` states that the Hausdorff distance is invariant under isometries. In other words, given any two sets `s` and `t` in a pseudometric space `α`, and an isometry `Φ` from `α` to another pseudometric space `β`, the Hausdorff distance between the images of `s` and `t` under `Φ` is the same as the Hausdorff distance between `s` and `t`. Isometry here means a map that preserves distances between elements of the sets. The Hausdorff distance between two sets is the smallest non-negative real number such that each set is included in the neighborhood of the other set extended by this number.
More concisely: The Hausdorff distance between the images of two sets under an isometry is equal to the Hausdorff distance between the original sets.
|
Metric.hausdorffDist_triangle'
theorem Metric.hausdorffDist_triangle' :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t u : Set α},
EMetric.hausdorffEdist t u ≠ ⊤ → Metric.hausdorffDist s u ≤ Metric.hausdorffDist s t + Metric.hausdorffDist t u
The theorem `Metric.hausdorffDist_triangle'` states that for any three sets `s`, `t`, and `u` in a pseudometric space `α`, assuming that the Hausdorff edistance between `t` and `u` is finite, the Hausdorff distance from set `s` to set `u` is less than or equal to the sum of the Hausdorff distance from `s` to `t` and the Hausdorff distance from `t` to `u`. This is the triangle inequality adapted for Hausdorff distances.
More concisely: Given any pseudometric space α and sets s, t, u with finite Hausdorff distance between t and u, the Hausdorff distance from s to u is less than or equal to the sum of the Hausdorff distances from s to t and t to u.
|
EMetric.infEdist_image
theorem EMetric.infEdist_image :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {x : α} {t : Set α}
{Φ : α → β}, Isometry Φ → EMetric.infEdist (Φ x) (Φ '' t) = EMetric.infEdist x t
The theorem `EMetric.infEdist_image` states that the minimum extended distance (also known as the infimum extended distance) from a point to a set is invariant under isometries. In other words, if `Φ` is an isometric map between two pseudoemetric spaces `α` and `β`, `x` is a point in `α`, and `t` is a set in `α`, then the minimum extended distance from the image of `x` under `Φ` to the image of the set `t` under `Φ` is the same as the minimum extended distance from `x` to `t`.
More concisely: Let `Φ` be an isometry between pseudometric spaces `(α, dα)` and `(β, dβ)`, `x ∈ α`, and `t ⊆ α`. Then `inf (dβ(Φ(x), Φ(s)) : s ∈ t) = inf (dα(x, s) : s ∈ t)`.
|
Metric.hausdorffDist_comm
theorem Metric.hausdorffDist_comm :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α}, Metric.hausdorffDist s t = Metric.hausdorffDist t s := by
sorry
The theorem `Metric.hausdorffDist_comm` states that for any type `α` that has a `PseudoMetricSpace` structure, and any two sets `s` and `t` of this type, the Hausdorff distance from `s` to `t` is equal to the Hausdorff distance from `t` to `s`. In other words, the Hausdorff distance between two sets is commutative in a pseudo metric space.
More concisely: In a pseudo-metric space, the Hausdorff distance between sets is commutative.
|
IsClosed.not_mem_iff_infDist_pos
theorem IsClosed.not_mem_iff_infDist_pos :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α},
IsClosed s → s.Nonempty → (x ∉ s ↔ 0 < Metric.infDist x s)
This theorem states that for any given closed set `s` in a pseudometric space and any point `x` in the space, the point `x` does not belong to the set `s` if and only if its infimum distance to the set `s` is greater than zero. In other words, a point is in a closed set if its minimum distance to the set is zero, and it is not in the set if its minimum distance to the set is positive. Note that the set must be nonempty for this to hold.
More concisely: A point in a pseudometric space is not in a closed set if and only if its minimum distance to the set is positive.
|
Metric.infEdist_ne_top
theorem Metric.infEdist_ne_top :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, s.Nonempty → EMetric.infEdist x s ≠ ⊤
This theorem states that in a pseudometric space, the minimal extended distance (infEdist) from a given point to a nonempty set is always finite. In other words, for any type `α` that forms a pseudometric space, any set `s` of type `α`, and any point `x` of type `α`, if the set `s` is not empty, then the infimum of the extended distances from `x` to any point in `s` cannot be infinity.
More concisely: In a pseudometric space, the infimum of the extended distances from a point to a nonempty set is finite.
|
Metric.infDist_le_infDist_of_subset
theorem Metric.infDist_le_infDist_of_subset :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {x : α},
s ⊆ t → s.Nonempty → Metric.infDist x t ≤ Metric.infDist x s
This theorem states that the minimal distance is monotone with respect to set inclusion in a pseudo metric space. More specifically, for any given type `α` equipped with a pseudo metric space structure, for any two sets `s` and `t` of this type, and any element `x` of this type, if `s` is a subset of `t` and `s` is not empty, then the minimal distance from `x` to `t` is less than or equal to the minimal distance from `x` to `s`. This theorem reflects the intuitive understanding that if we extend a set, the minimal distance of a point to the set does not increase.
More concisely: In a pseudo metric space, for any set `s` subset and non-empty `s`, and any `x` and `t` in the underlying type, if `s` is a subset of `t`, then `d(x,s) ≤ d(x,t)`.
|
Metric.exists_dist_lt_of_hausdorffDist_lt'
theorem Metric.exists_dist_lt_of_hausdorffDist_lt' :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {y : α} {r : ℝ},
y ∈ t → Metric.hausdorffDist s t < r → EMetric.hausdorffEdist s t ≠ ⊤ → ∃ x ∈ s, dist x y < r
The theorem `Metric.exists_dist_lt_of_hausdorffDist_lt'` states that for any type `α` equipped with a `PseudoMetricSpace` structure, given two sets `s` and `t` of this type, a real number `r`, and an element `y` of the set `t`, if the Hausdorff distance between `s` and `t` is less than `r` and the Hausdorff edistance between `s` and `t` is not infinite, then there exists an element `x` in the set `s` such that the distance between `x` and `y` is less than `r`.
In simpler terms, if the overall distance between two sets is less than a certain value, and these sets are not infinitely far apart, then you can always find a point in one set that is closer than this value to a given point in the other set.
More concisely: Given a PseudoMetricSpace `α` with sets `s` and `t`, real `r`, and an element `y` in `t`, if Hausdorff distance `d(s,t)` is less than `r` and finite, then there exists an `x` in `s` with `d(x,y)` less than `r`.
|
EMetric.hausdorffEdist_le_of_infEdist
theorem EMetric.hausdorffEdist_le_of_infEdist :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α} {r : ENNReal},
(∀ x ∈ s, EMetric.infEdist x t ≤ r) → (∀ x ∈ t, EMetric.infEdist x s ≤ r) → EMetric.hausdorffEdist s t ≤ r
The theorem `EMetric.hausdorffEdist_le_of_infEdist` states that for any two sets `s` and `t` in a Pseudo Emetric Space and a given extended nonnegative real number `r`, if for every point `x` in set `s`, the minimal extended distance (`infEdist`) from `x` to the set `t` is less than or equal to `r`, and similarly, for every point `x` in set `t`, the minimal extended distance from `x` to the set `s` is less than or equal to `r`, then the Hausdorff extended distance (`hausdorffEdist`) between the two sets is less than or equal to `r`.
In other words, the theorem provides a way to bound the Hausdorff distance between two sets by simply bounding the minimal extended distance of any point in each set to the other set. This theorem is especially valuable in the analysis of metric spaces.
More concisely: If for every point in set $s$ the infimum of the extended distances to set $t$ is less than or equal to $r$, and similarly for set $t$ to set $s$, then the Hausdorff extended distance between $s$ and $t$ is less than or equal to $r$.
|
Metric.infDist_zero_of_mem
theorem Metric.infDist_zero_of_mem :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, x ∈ s → Metric.infDist x s = 0
This theorem states that for any given point `x` and a set `s` in a pseudo metric space `α`, if the point `x` belongs to the set `s`, then the minimal distance from the point `x` to the set `s`, denoted as `Metric.infDist x s`, is equal to zero. In other words, the smallest distance between a point and a set that the point is a member of is always zero in any pseudo metric space.
More concisely: In a pseudo metric space, the distance from a point to a set containing that point is zero.
|
Metric.infDist_le_infDist_add_dist
theorem Metric.infDist_le_infDist_add_dist :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x y : α},
Metric.infDist x s ≤ Metric.infDist y s + dist x y
This theorem states that for any pseudo metric space, the minimum distance from a point `x` to a set `s` is always less than or equal to the minimum distance from another point `y` to the same set `s`, plus the distance between `x` and `y`. This theorem, for a space that respects the properties of a pseudo metric, provides an upper bound on the minimal distance from a point to a set using the distance to another reference point and the distance from this reference point to the original point.
More concisely: For any pseudo metric space, the distance from a point to a set is less than or equal to the distance from another point to the same set plus the distance between the two points.
|
EMetric.hausdorffEdist_empty
theorem EMetric.hausdorffEdist_empty :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, s.Nonempty → EMetric.hausdorffEdist s ∅ = ⊤
The theorem `EMetric.hausdorffEdist_empty` states that for any non-empty set `s` of type `α` in a PseudoEMetricSpace, the Hausdorff edistance between `s` and the empty set is infinite. In other words, there is no finite `r` such that every point in `s` is within `r` distance of some point in the empty set, and vice versa, hence the edistance is represented by the infinite value `⊤` in the extended nonnegative real number system `ENNReal`.
More concisely: The Hausdorff distance between a non-empty set in a PseudoEMetricSpace and the empty set is infinite.
|
IsClosed.mem_iff_infDist_zero
theorem IsClosed.mem_iff_infDist_zero :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α},
IsClosed s → s.Nonempty → (x ∈ s ↔ Metric.infDist x s = 0)
This theorem states that for any point `x` and any closed set `s` in a pseudo metric space `α`, `x` belongs to `set` `s` if and only if the minimum distance from `x` to `s` is zero. This implies that the point is either a member of the set or is arbitrarily close to the set such that the minimum distance to the set is effectively zero. To apply this theorem, `s` must be a nonempty closed set.
More concisely: A point in a pseudo metric space belongs to a nonempty closed set if and only if the minimum distance to the set is zero.
|
Metric.infDist_le_dist_of_mem
theorem Metric.infDist_le_dist_of_mem :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x y : α}, y ∈ s → Metric.infDist x s ≤ dist x y
This theorem states that for any given type `α`, which is a pseudo metric space, and for any set `s` of this type, and any two elements `x` and `y` of this type, if `y` is a member of set `s`, then the minimal distance from `x` to the set `s` is less than or equal to the distance from `x` to `y`. This theorem ensures that the minimal distance from a point to a set will never exceed the distance from that point to any specific member of the set.
More concisely: For any pseudo-metric space `(α, d)` and set `s ⊆ α`, and for all `x, y ∈ α` with `y ∈ s`, we have `d(x, s) ≤ d(x, y)`.
|
EMetric.hausdorffEdist_image
theorem EMetric.hausdorffEdist_image :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {s t : Set α} {Φ : α → β},
Isometry Φ → EMetric.hausdorffEdist (Φ '' s) (Φ '' t) = EMetric.hausdorffEdist s t
The theorem `EMetric.hausdorffEdist_image` states that the Hausdorff edistance, which is the smallest value `r` such that each set is contained in the `r`-neighborhood of the other, is invariant under isometries. In other words, given two sets `s` and `t` of elements from a space with a pseudoemetric (a generalized concept of distance that may take the value infinity), and an isometry `Φ` (a transformation that preserves distances), the Hausdorff edistance between the image of `s` and the image of `t` under `Φ` is equal to the Hausdorff edistance between `s` and `t` itself. This essentially means that the "distance" between the two sets remains unchanged, when the entire space is transformed by an isometry.
More concisely: The Hausdorff distance between the images of two sets under an isometry is equal to the Hausdorff distance between the original sets.
|
Metric.infDist_le_infDist_add_hausdorffDist
theorem Metric.infDist_le_infDist_add_hausdorffDist :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {x : α},
EMetric.hausdorffEdist s t ≠ ⊤ → Metric.infDist x t ≤ Metric.infDist x s + Metric.hausdorffDist s t
The theorem `Metric.infDist_le_infDist_add_hausdorffDist` asserts that for any pseudometric space `α`, any two sets `s` and `t` in `α`, and any point `x` in `α`, provided that the Hausdorff e-distance between `s` and `t` is not infinite, the infimum distance from `x` to `t` is less than or equal to the sum of the infimum distance from `x` to `s` and the Hausdorff distance between `s` and `t`. In simpler words, the shortest distance to a set `t` from a point `x` is at most the shortest distance to another set `s` from the same point `x` plus the smallest distance such that each set is included in the neighborhood of the other.
More concisely: For any pseudometric space, given sets `s` and `t`, and a point `x`, if the Hausdorff distance between `s` and `t` is finite, then the infimum distance from `x` to `s` plus the Hausdorff distance between `s` and `t` is greater than or equal to the infimum distance from `x` to `t`. (Note: The Lean theorem statement has the inequality reversed.)
|
Metric.hausdorffDist_triangle
theorem Metric.hausdorffDist_triangle :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t u : Set α},
EMetric.hausdorffEdist s t ≠ ⊤ → Metric.hausdorffDist s u ≤ Metric.hausdorffDist s t + Metric.hausdorffDist t u
The theorem `Metric.hausdorffDist_triangle` states that the Hausdorff distance satisfies the triangle inequality. In more detail, for any three sets `s`, `t`, and `u` in a pseudo-metric space, if the extended (possibly infinite) Hausdorff distance between `s` and `t` is not infinity, then the Hausdorff distance from `s` to `u` is less than or equal to the sum of the Hausdorff distance from `s` to `t` and the Hausdorff distance from `t` to `u`. This is an extension of the classic triangle inequality in metric spaces to the context of Hausdorff distances between sets.
More concisely: For any sets $s$, $t$, and $u$ in a pseudo-metric space, if $d_{Haus}(s, t) < \infty$, then $d_{Haus}(s, u) \leq d_{Haus}(s, t) + d_{Haus}(t, u)$.
|
Metric.infDist_zero_of_mem_closure
theorem Metric.infDist_zero_of_mem_closure :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, x ∈ closure s → Metric.infDist x s = 0
This theorem states that if a point belongs to the closure of a set `s` in a pseudometric space, then the infimum distance (or the shortest distance) of that point to the set `s` is zero. In other words, for any point that is an element of the closure of a set `s`, the point is as close as possible (distance zero) to the set `s`. The converse, that if the infimum distance of a point to `s` is zero then the point belongs to the closure of `s`, is also true provided that the set `s` is not empty.
More concisely: In a pseudometric space, a point belongs to the closure of a set if and only if its minimum distance to the set is zero, provided the set is non-empty.
|
EMetric.mem_closure_iff_infEdist_zero
theorem EMetric.mem_closure_iff_infEdist_zero :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, x ∈ closure s ↔ EMetric.infEdist x s = 0 := by
sorry
This theorem states that in the context of a pseudoemetric space, a point belongs to the closure of a set if and only if its infimum extended distance (infimum edistance) to the set is zero. In more detail, for any type `α` that forms a pseudoemetric space, for any point `x` of type `α`, and for any set `s` of elements of type `α`, `x` is an element of the closure of `s` if and only if the infimum of the extended distances from `x` to any point in `s` is zero. This connects the concept of closure in a topological space with the concept of distance in a metric space, suggesting that the closure of a set can be thought of as including all points that are "infinitely close" to that set.
More concisely: In a pseudometric space, a point belongs to the closure of a set if and only if its infimum extended distance to the set is zero.
|
Metric.infDist_empty
theorem Metric.infDist_empty : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α}, Metric.infDist x ∅ = 0
This theorem states that, for any point 'x' in a pseudometric space 'α', the minimal distance from 'x' to an empty set is always 0. In the context of metric spaces, it seems more reasonable to have the minimal distance to an empty set as infinity, which can be obtained using `EMetric.infEdist` instead of `Metric.infDist`, as the former can take values in the extended nonnegative real numbers including infinity (`ℝ≥0∞`).
More concisely: In a pseudometric space, the distance from any point to the empty set is 0.
|
Metric.infDist_image
theorem Metric.infDist_image :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {t : Set α} {x : α}
{Φ : α → β}, Isometry Φ → Metric.infDist (Φ x) (Φ '' t) = Metric.infDist x t
The theorem `Metric.infDist_image` states that the infimum distance is invariant under isometries. More specifically, for any two pseudometric spaces `α` and `β`, a set `t` in `α`, a point `x` in `α`, and an isometry `Φ` from `α` to `β`, the infimum distance from `Φ(x)` to the image of `t` under `Φ` is equal to the infimum distance from `x` to `t`. This means that applying an isometry to a point and a set doesn't change the minimal distance of the point to the set, which aligns with the intuition that isometries preserve distances.
More concisely: Given isometric maps $\Phi:\ (X, d_X) \rightarrow (Y, d_Y)$, points $x \in X$ and $t \in X$, the infimum of distances from $x$ to $t$ in $(X, d_X)$ equals the infimum of distances from $\Phi(x)$ to $\Phi(t)$ in $(Y, d_Y)$.
|
EMetric.infEdist_empty
theorem EMetric.infEdist_empty : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, EMetric.infEdist x ∅ = ⊤ := by
sorry
This theorem states that for any type `α` that is a PseudoEMetricSpace, the minimal extended distance (`infEdist`) from any given point `x` of type `α` to an empty set is infinity (`⊤`). In other words, in the context of a pseudo-metric space, if we try to find the smallest distance from a point to all points in an empty set, the result is always infinity.
More concisely: For any pseudo-metric space `(α, edist)`, the infimum of distances from a point `x ∈ α` to the empty set is infinity.
|
EMetric.hausdorffEdist_triangle
theorem EMetric.hausdorffEdist_triangle :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t u : Set α},
EMetric.hausdorffEdist s u ≤ EMetric.hausdorffEdist s t + EMetric.hausdorffEdist t u
The theorem `EMetric.hausdorffEdist_triangle` states that the Hausdorff distance in a PseudoEMetricSpace satisfies the triangle inequality. In more specific terms, for any three sets of elements `s`, `t`, and `u` in a given PseudoEMetricSpace `α`, the Hausdorff distance (the smallest `r` such that each set is contained in the `r`-neighborhood of the other one) between `s` and `u` is less than or equal to the sum of the Hausdorff distances between `s` and `t`, and `t` and `u`. This is a formal statement of the geometric principle that the direct path between two points is never longer than the path that goes through an intermediate point.
More concisely: In a PseudoEMetricSpace, the Hausdorff distance between any two sets is less than or equal to the sum of the Hausdorff distances between each pair of adjacent sets.
|
Metric.continuous_infNndist_pt
theorem Metric.continuous_infNndist_pt :
∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), Continuous fun x => Metric.infNndist x s
This theorem states that the minimal distance from a point to a set is a continuous function. Specifically, for a certain set 's' within a pseudometric space (a generalized concept of a metric space), the function that measures the minimal distance from any point 'x' to set 's' is a continuous function. In mathematical terms, this means that for any small change in the location of 'x', there will be a correspondingly small change in the computed minimal distance to the set 's'.
More concisely: The function that maps each point to the minimal distance from that point to a given set is a continuous function in a pseudometric space.
|
EMetric.exists_edist_lt_of_hausdorffEdist_lt
theorem EMetric.exists_edist_lt_of_hausdorffEdist_lt :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α} {r : ENNReal},
x ∈ s → EMetric.hausdorffEdist s t < r → ∃ y ∈ t, edist x y < r
The theorem `EMetric.exists_edist_lt_of_hausdorffEdist_lt` states that for any given type `α` with a `PseudoEMetricSpace` structure, any two sets `s` and `t` of this type, any point `x` from set `s`, and any extended non-negative real number `r`, if the Hausdorff distance between set `s` and `t` is less than `r`, and `x` is an element of set `s`, then there exists a point `y` in set `t` such that the extended metric distance between point `x` and `y` is less than `r`. In other words, if the Hausdorff distance between two sets is less than a certain value, then for each point in one set, there is a corresponding point in the other set whose distance is also less than that value.
More concisely: Given a PseudoEMetricSpace α, if Hausdorff distance between sets s and t is less than r and x ∈ s, then there exists y ∈ t such that edist x y < r.
|
Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded
theorem Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
s.Nonempty → t.Nonempty → Bornology.IsBounded s → Bornology.IsBounded t → EMetric.hausdorffEdist s t ≠ ⊤
The theorem `Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded` states that in any pseudo-metric space `α`, if two sets `s` and `t` are both nonempty and bounded, then the Hausdorff edistance between these two sets is not infinite. In other words, the Hausdorff edistance, which is the smallest radius `r` such that each set is contained in the `r`-neighborhood of the other one, is always a finite value for any two nonempty, bounded sets in a pseudo-metric space.
More concisely: In any pseudo-metric space, the Hausdorff distance between two nonempty and bounded sets is finite.
|
EMetric.mem_iff_infEdist_zero_of_closed
theorem EMetric.mem_iff_infEdist_zero_of_closed :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, IsClosed s → (x ∈ s ↔ EMetric.infEdist x s = 0)
This theorem states that for any type `α` that has a pseudo emetric space structure, a point `x` of type `α`, and a closed set `s` of points of type `α`, `x` belongs to `s` if and only if the infimum extended distance from `x` to the set `s` is zero. In other words, in a pseudo emetric space, a point is contained in a closed set if its minimal distance to the set is zero.
More concisely: In a pseudo-metric space, a point belongs to a closed set if and only if its pseudo-distance to the set is 0.
|
Metric.hausdorffDist_le_of_mem_dist
theorem Metric.hausdorffDist_le_of_mem_dist :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {r : ℝ},
0 ≤ r → (∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r) → (∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r) → Metric.hausdorffDist s t ≤ r
The theorem `Metric.hausdorffDist_le_of_mem_dist` states that for any type `α` which is a pseudo metric space, given two sets `s` and `t` of type `α`, and a nonnegative real number `r`, if for every element `x` in set `s` there exists an element `y` in set `t` such that the distance between `x` and `y` is less than or equal to `r`, and similarly, for every element `x` in set `t` there exists an element `y` in set `s` such that the distance between `x` and `y` is less than or equal to `r`, then the Hausdorff distance (which is the greatest of all the distances from a point in one set to the closest point in the other set) between the two sets `s` and `t` is less than or equal to `r`.
More concisely: If sets `s` and `t` in a pseudo metric space have the property that for every element `x` in `s` there exists an element `y` in `t` with distance less than or equal to `r` and vice versa, then the Hausdorff distance between `s` and `t` is less than or equal to `r`.
|
Metric.infDist_le_hausdorffDist_of_mem
theorem Metric.infDist_le_hausdorffDist_of_mem :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {x : α},
x ∈ s → EMetric.hausdorffEdist s t ≠ ⊤ → Metric.infDist x t ≤ Metric.hausdorffDist s t
This theorem states that for any given type `α` that is a PseudoMetricSpace (a set of objects with a distance function that satisfies certain properties), two sets of this type `s` and `t`, and an element `x` of type `α` that belongs to set `s`, if the Hausdorff extended metric distance between sets `s` and `t` is not infinite, then the infimum distance (minimal distance) between the point `x` and set `t` is less than or equal to the Hausdorff distance between the sets `s` and `t`. In other words, the distance from a point to a set is no greater than the Hausdorff distance between the set containing the point and the other set.
More concisely: For any PseudoMetricSpace `α` and sets `s`, `t` of type `α`, if `x` is an element of `s` and the Hausdorff distance between `s` and `t` is finite, then the infimum distance from `x` to `t` is less than or equal to the Hausdorff distance between `s` and `t`.
|
EMetric.infEdist_zero_of_mem
theorem EMetric.infEdist_zero_of_mem :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, x ∈ s → EMetric.infEdist x s = 0
The theorem `EMetric.infEdist_zero_of_mem` states that for any type `α` that forms a pseudo extended metric space, and for any point `x` of type `α` belonging to a set `s` of type `α`, the extended minimum ('infimum') distance from `x` to `s` is zero. In other words, if a point is a member of a given set within a pseudo extended metric space, its minimum distance to the set is always zero.
More concisely: For any pseudo extended metric space `(α, d)` and set `s ⊆ α`, the infimum of distances from any point `x ∈ s` to `s` is 0.
|
EMetric.infEdist_lt_iff
theorem EMetric.infEdist_lt_iff :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α} {r : ENNReal},
EMetric.infEdist x s < r ↔ ∃ y ∈ s, edist x y < r
This theorem states that in any pseudo-emetric space `α`, for any point `x` of type `α`, any set `s` of type `α`, and any extended nonnegative real number `r`, the minimal edistance (`EMetric.infEdist`) from point `x` to the set `s` is less than `r` if and only if there exists a point `y` in the set `s` such that the edistance from `x` to `y` is less than `r`. In other words, the smallest distance from a point to a set is less than a given value if and only if there is some point in the set that is less than that given value away.
More concisely: In a pseudo-metric space, the infimum of the distances from a point to a set equals the minimum distance to any point in the set.
|
EMetric.nonempty_of_hausdorffEdist_ne_top
theorem EMetric.nonempty_of_hausdorffEdist_ne_top :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
s.Nonempty → EMetric.hausdorffEdist s t ≠ ⊤ → t.Nonempty
This theorem states that if we have a nonempty set `s` and another set `t` in a pseudo extended metric space, and if the Hausdorff extended distance between these two sets is finite (not infinity), then set `t` must also be nonempty. The Hausdorff extended distance is the smallest possible distance such that each set is contained within the other set's neighborhood of that distance. In other words, a set cannot have a finite Hausdorff distance to a nonempty set if it is empty itself.
More concisely: If `s` is a nonempty set and the Hausdorff extended distance between `s` and a set `t` in a pseudo extended metric space is finite, then `t` is also nonempty.
|
Metric.lipschitz_infDist_pt
theorem Metric.lipschitz_infDist_pt :
∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), LipschitzWith 1 fun x => Metric.infDist x s
This theorem states that for any set `s` in a pseudometric space `α`, the function `Metric.infDist x s` that computes the infimum (or minimal) distance from a point `x` to the set `s` is Lipschitz continuous with a Lipschitz constant of `1`. In other words, for any two points `x` and `y` in `α`, the difference in the infimum distances of `x` and `y` from the set `s` is at most the distance between `x` and `y`. This is expressed in the following inequality: `| Metric.infDist x s - Metric.infDist y s | ≤ | x - y |`.
More concisely: The infimum distance function from a point to a set in a pseudometric space is Lipschitz continuous with Lipschitz constant 1. That is, |Metric.infDist x s - Metric.infDist y s| ≤ |x - y| for all x, y in the pseudometric space and any set s.
|
Metric.mem_closure_iff_infDist_zero
theorem Metric.mem_closure_iff_infDist_zero :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α},
s.Nonempty → (x ∈ closure s ↔ Metric.infDist x s = 0)
This theorem states that for any type `α` equipped with a pseudo metric space structure, for any set `s` of `α`, and for any point `x` of `α`, if the set `s` is nonempty, then the point `x` belongs to the closure of the set `s` if and only if the infimum distance of the point `x` to the set `s` is zero. In other words, a point is in the closure of a set if its minimum distance to the set is zero, provided the set is nonempty. The closure of a set is the smallest closed set containing the set. The infimum distance is the smallest possible distance between a point and a set in a pseudo metric space.
More concisely: For any pseudo metric space `(α, d)` and nonempty set `s ∈ α`, a point `x ∈ α` belongs to the closure of `s` if and only if the infimum distance `��բ(x, s) = 0`.
|
Metric.infDist_closure
theorem Metric.infDist_closure :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α},
Metric.infDist x (closure s) = Metric.infDist x s
The theorem `Metric.infDist_closure` states that for any type `α` which forms a PseudoMetricSpace, for any set `s` of type `α` and for any element `x` of the same type, the minimal distance from `x` to the closure of `s` equals the minimal distance from `x` to `s`. In other words, the smallest distance between a point and a given set remains the same even when the set is extended to its closure. A closure of a set is the smallest closed set that contains the original set.
More concisely: For any PseudoMetricSpace `α`, and set `s` in `α` with closure `cl(s)`, the infimum of the distances from any point `x` in `α` to `s` equals the infimum of the distances from `x` to `cl(s)`.
|
EMetric.infEdist_le_infEdist_add_hausdorffEdist
theorem EMetric.infEdist_le_infEdist_add_hausdorffEdist :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α},
EMetric.infEdist x t ≤ EMetric.infEdist x s + EMetric.hausdorffEdist s t
The theorem `EMetric.infEdist_le_infEdist_add_hausdorffEdist` states that for any pseudo-extended metric space `α` and any sets `s` and `t` in this space, as well as any point `x` in this space, the extended distance from `x` to `t` is always less than or equal to the extended distance from `x` to `s` plus the Hausdorff (greatest shortest) distance between the sets `s` and `t`. Here, the concept of extended distance allows for the consideration of infinitely distant points, and the Hausdorff distance between two sets is the greatest of all the shortest distances from a point in one set to the other set.
More concisely: For any pseudo-extended metric space, extended distance from a point to a set plus Hausdorff distance between the sets is an upper bound for the extended distance from that point to any other set.
|
EMetric.infEdist_singleton
theorem EMetric.infEdist_singleton :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α}, EMetric.infEdist x {y} = edist x y
This theorem states that for any point `x` and another point `y` in a `PseudoEMetricSpace` (which is a generalization of a metric space that allows possibly infinite distances), the infimum extended distance (or the smallest extended distance) from `x` to the singleton set containing just `y`, is equal to the extended distance from `x` to `y`. In simpler terms, the shortest distance from a point to a set containing a single point, is just the distance between the two points.
More concisely: For any `x` and `y` in a `PseudoEMetricSpace`, the infimum of the extended distances from `x` to the singleton set {`y`} equals the extended distance from `x` to `y`.
|
EMetric.hausdorffEdist_def
theorem EMetric.hausdorffEdist_def :
∀ {α : Type u_2} [inst : PseudoEMetricSpace α] (s t : Set α),
EMetric.hausdorffEdist s t = (⨆ x ∈ s, EMetric.infEdist x t) ⊔ ⨆ y ∈ t, EMetric.infEdist y s
This theorem states that for any given type `α` equipped with a pseudo extended metric space structure, and any two sets `s` and `t` of type `α`, the Hausdorff extended distance between `s` and `t` is defined as the supremum of the infimum extended distances from each point in `s` to the set `t`, and vice versa. In other words, it provides a characterisation of the Hausdorff distance in terms of minimal distances of points to sets.
More concisely: The Hausdorff distance between two sets in a pseudo extended metric space is the supremum of the infimum of extended distances from each point in one set to the other, and the supremum of the infimum of extended distances from each point in the other set to the first set.
|
EMetric.hausdorffEdist_zero_iff_closure_eq_closure
theorem EMetric.hausdorffEdist_zero_iff_closure_eq_closure :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
EMetric.hausdorffEdist s t = 0 ↔ closure s = closure t
This theorem states that in any pseudo-emetric space (a generalization of metric spaces which allows infinite distances), two sets have zero Hausdorff distance if and only if they have the same closure. The Hausdorff distance is a way to define a distance between sets of points, and in this case, zero distance implies that each set is contained within the infinitesimal neighborhood of the other. The closure of a set is the smallest closed set that contains the set, adding in limit points. Thus, if two sets have the same closure, then they are "effectively" the same set from the viewpoint of the Hausdorff distance.
More concisely: In a pseudo-metric space, two sets have zero Hausdorff distance if and only if they have equal closures.
|
EMetric.hausdorffEdist_le_ediam
theorem EMetric.hausdorffEdist_le_ediam :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
s.Nonempty → t.Nonempty → EMetric.hausdorffEdist s t ≤ EMetric.diam (s ∪ t)
This theorem states that for any type `α` equipped with a `PseudoEMetricSpace` structure, and any two nonempty sets `s` and `t` of this type, the Hausdorff distance between `s` and `t` is less than or equal to the diameter of the union of `s` and `t`. In mathematical terms, the Hausdorff distance, which is the smallest `r` such that each set is contained in the `r`-neighborhood of the other, is always less than or equal to the largest distance between any two points in the set formed by combining `s` and `t`.
More concisely: For any `PseudoEMetricSpace` `α` and nonempty sets `s` and `t` of type `α`, the Hausdorff distance between `s` and `t` is less than or equal to the diameter of their union.
|
Metric.hausdorffDist_zero_iff_closure_eq_closure
theorem Metric.hausdorffDist_zero_iff_closure_eq_closure :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
EMetric.hausdorffEdist s t ≠ ⊤ → (Metric.hausdorffDist s t = 0 ↔ closure s = closure t)
The theorem `Metric.hausdorffDist_zero_iff_closure_eq_closure` states that for any two sets `s` and `t` in a pseudometric space (a generalization of the concept of a metric space), if the Hausdorff extended metric distance between `s` and `t` is not infinity, then the Hausdorff distance between `s` and `t` is zero if and only if the closure of `s` is the same as the closure of `t`. In the context of this theorem, the "closure" of a set is the smallest closed set that contains the original set, and the "Hausdorff distance" quantifies how far apart two subsets of a metric space are from each other.
More concisely: In a pseudometric space, the closures of two sets have equal closure if and only if their Hausdorff distance is zero, provided the Hausdorff distance is finite.
|
EMetric.continuous_infEdist
theorem EMetric.continuous_infEdist :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, Continuous fun x => EMetric.infEdist x s
The theorem `EMetric.continuous_infEdist` states that for any type 'α' that is a pseudo-emetric space and any set 's' of type 'α', the function that maps a point 'x' to the minimum extended distance (or edist) from 'x' to the set 's' is continuous. In simpler terms, it says that the smallest distance from any given point to a particular set varies smoothly as you move the point around.
More concisely: The function that maps a point in a pseudo-metric space to the minimum extended distance from that point to a given set is continuous.
|
Metric.infDist_nonneg
theorem Metric.infDist_nonneg :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, 0 ≤ Metric.infDist x s
The theorem `Metric.infDist_nonneg` states that for any type `α` equipped with a pseudo-metric space structure, any set `s` of elements of type `α`, and any element `x` of type `α`, the minimal distance from `x` to the set `s` is always nonnegative. Here, the minimal distance is defined using the `Metric.infDist` function, which converts the infimum extended distance to a real number. In mathematical terms, this asserts that for all $x \in \alpha$ and for any set $s \subseteq \alpha$, we have $0 \leq \text{infDist}(x, s)$, where $\text{infDist}(x, s)$ denotes the minimum distance from `x` to `s`.
More concisely: For any pseudo-metric space (α, d), and any set s ⊆ α and x ∈ α, the infimum of the distances from x to s is non-negative.
|
Mathlib.Topology.MetricSpace.HausdorffDistance._auxLemma.26
theorem Mathlib.Topology.MetricSpace.HausdorffDistance._auxLemma.26 :
∀ (x : ENNReal), (x.toReal = 0) = (x = 0 ∨ x = ⊤)
This theorem states that for every extended nonnegative real number `x` (which is usually denoted [0, ∞] and is the codomain of a measure), `x` being converted to a real number equals zero if and only if `x` equals zero or `x` equals positive infinity. In other words, in the extended nonnegative real numbers, the only values that become zero when converted to real numbers are zero and positive infinity.
More concisely: In the extended nonnegative real numbers, a number converts to zero in the real numbers if and only if it is either zero or positive infinity.
|
Metric.uniformContinuous_infNndist_pt
theorem Metric.uniformContinuous_infNndist_pt :
∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), UniformContinuous fun x => Metric.infNndist x s
The theorem `Metric.uniformContinuous_infNndist_pt` states that for any pseudo metric space `α` and any set `s` of points in `α`, the function that calculates the minimal non-negative real number distance (`ℝ≥0`) from a point `x` in `α` to the set `s`, denoted as `Metric.infNndist x s`, is uniformly continuous. In other words, if two points are close to each other in the pseudo metric space `α`, then their minimal distances to the set `s` are also close to each other, regardless of where these points are located in `α`. The function `Metric.infNndist x s` changes smoothly across the pseudo metric space `α`.
More concisely: The function `Metric.infNndist x : α → ℝ≥0` that maps each point `x` in a pseudo metric space `α` to the minimum distance from `x` to a given set `s` in `α` is uniformly continuous.
|
IsClosed.hausdorffDist_zero_iff_eq
theorem IsClosed.hausdorffDist_zero_iff_eq :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
IsClosed s → IsClosed t → EMetric.hausdorffEdist s t ≠ ⊤ → (Metric.hausdorffDist s t = 0 ↔ s = t)
The theorem `IsClosed.hausdorffDist_zero_iff_eq` states that for any two closed sets `s` and `t` in a pseudometric space `α`, if the Hausdorff extended metric between `s` and `t` is not infinite, then the Hausdorff distance between `s` and `t` is zero if and only if the sets `s` and `t` are identical. In other words, in a pseudometric space, two closed sets are exactly the same if they have a Hausdorff distance of zero, assuming the Hausdorff extended metric between them is not infinite.
More concisely: In a pseudometric space, two closed sets have zero Hausdorff distance if and only if they are identical, given that their Hausdorff extended metric is finite.
|
Metric.hausdorffDist_closure
theorem Metric.hausdorffDist_closure :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
Metric.hausdorffDist (closure s) (closure t) = Metric.hausdorffDist s t
This theorem states that in every pseudo-metric space, the Hausdorff distance between two sets and the Hausdorff distance between their closures are the same. In other words, closing the two sets does not change their Hausdorff distance. The Hausdorff distance is the smallest non-negative real number such that each set is included in the neighborhood of the other set with radius equal to this number. The closure of a set is the smallest closed set that contains the original set.
More concisely: In every pseudo-metric space, the Hausdorff distance between two sets equals the Hausdorff distance between their closures.
|
EMetric.hausdorffEdist_self_closure
theorem EMetric.hausdorffEdist_self_closure :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, EMetric.hausdorffEdist s (closure s) = 0
This theorem states that for any set `s` in a pseudo emetric space `α`, the Hausdorff edistance between the set `s` and its closure is zero. In other words, in the given pseudo emetric space, the minimum distance required such that each set (`s` and its closure) is contained in the neighborhood of the other is always zero.
More concisely: In a pseudo metric space, the Hausdorff distance between a set and its closure is zero.
|
Metric.hausdorffDist_nonneg
theorem Metric.hausdorffDist_nonneg :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α}, 0 ≤ Metric.hausdorffDist s t
The theorem `Metric.hausdorffDist_nonneg` states that for any type `α` which forms a PseudoMetricSpace, and any two sets `s` and `t` of this type `α`, the Hausdorff distance between these two sets is always nonnegative. In mathematical terms, for all `s, t ∈ Set α`, where `α` is a PseudoMetricSpace, it holds that `0 ≤ Metric.hausdorffDist s t`.
More concisely: For any two sets `s` and `t` in a pseudo-metric space `α`, the Hausdorff distance between them is non-negative. (i.e., `0 ≤ Metric.hausdorffDist s t`)
|
Metric.infDist_singleton
theorem Metric.infDist_singleton :
∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, Metric.infDist x {y} = dist x y
This theorem states that the minimal distance from a point to a singleton set, in a pseudo metric space, is equal to the distance to the unique point in that singleton set. In more specific terms, for all types `α` that have a `PseudoMetricSpace` instance and for any two points `x` and `y` of type `α`, the minimal distance `Metric.infDist` from `x` to the singleton set containing only `y` is equal to the distance `dist` between `x` and `y`.
More concisely: In a pseudo metric space, the minimal distance from a point to a singleton set equals the distance to the unique point in that set.
|
EMetric.infEdist_closure
theorem EMetric.infEdist_closure :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α},
EMetric.infEdist x (closure s) = EMetric.infEdist x s
This theorem states that for any pseudometric space `α` and any set `s` of elements from `α`, the infimum extended distance (infimum of all the distances) of a point `x` from `α` to the closure of `s` is equal to the infimum extended distance of the point `x` to the set `s` itself. In other words, the minimum possible extended distance from any point to a set and its closure (the smallest closed set containing the original set) are the same.
More concisely: For any pseudometric space `α` and point `x` in `α`, the infimum of the extended distances from `x` to `s` and `x` to the closure of `s` is equal.
|
EMetric.hausdorffEdist_zero_iff_eq_of_closed
theorem EMetric.hausdorffEdist_zero_iff_eq_of_closed :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
IsClosed s → IsClosed t → (EMetric.hausdorffEdist s t = 0 ↔ s = t)
This theorem states that for any two closed sets `s` and `t` in a pseudo-emetric space `α`, the Hausdorff edistance between `s` and `t` is equal to zero if and only if `s` and `t` are the same set. The Hausdorff edistance is a measure of the 'distance' between two sets, defined as the smallest 'r' such that each set is contained in the 'r'-neighborhood of the other. Here, a set being 'closed' means it contains all its limit points.
More concisely: In a pseudometric space, two closed sets have Hausdorff distance equal to zero if and only if they are equal.
|
EMetric.exists_real_pos_lt_infEdist_of_not_mem_closure
theorem EMetric.exists_real_pos_lt_infEdist_of_not_mem_closure :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {E : Set α},
x ∉ closure E → ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < EMetric.infEdist x E
The theorem `EMetric.exists_real_pos_lt_infEdist_of_not_mem_closure` states that for any type `α` equipped with a pseudo-emetric space structure, and for any element `x` of type `α` and any set `E` of type `α`, if `x` is not in the closure of `E`, then there exists a real number `ε` such that `ε` is greater than zero and the extended non-negative real number corresponding to `ε` is less than the infimum extended distance from `x` to `E`. In simpler terms, if a point is not in the closure of a set, then there is a positive distance between the point and the set.
More concisely: If `α` is a pseudo-metric space, `x` is not in the closure of `E ⊆ α`, then there exists `ε > 0` such that inf{d(x, y) : y ∈ E} > ε.
|
EMetric.infEdist_union
theorem EMetric.infEdist_union :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α},
EMetric.infEdist x (s ∪ t) = EMetric.infEdist x s ⊓ EMetric.infEdist x t
This theorem states that for any given type `α` that has a `PseudoEMetricSpace` structure, a point `x` of type `α`, and two sets `s` and `t` of type `α`, the extended distance from `x` to the union of `s` and `t` is equal to the infimum (greatest lower bound) of the extended distance from `x` to `s` and the extended distance from `x` to `t`. This means that the shortest distance from a point to a union of two sets is the minimum of the shortest distances to each of the sets.
More concisely: For any `PseudoEMetricSpace` `α`, point `x` in `α`, and sets `s`, `t` in `α`, the extended distance from `x` to `s ∪ t` equals the infimum of the extended distances from `x` to `s` and `x` to `t`. In other words, the distance from `x` to the union of `s` and `t` is the minimum of the distances from `x` to each set.
|
Metric.hausdorffDist_empty'
theorem Metric.hausdorffDist_empty' :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Metric.hausdorffDist ∅ s = 0
The theorem `Metric.hausdorffDist_empty'` states that the Hausdorff distance, as defined in the context of a pseudometric space, between any given set `s` and the empty set is always zero. This definition is using the real valued version of the Hausdorff distance, `Metric.hausdorffDist`, which takes values in the reals. If one wishes to use the extended nonnegative real valued version of the Hausdorff distance, which might give a more intuitive value of infinity between the empty set and a nonempty set, one should use `EMetric.hausdorffEdist` instead.
More concisely: In a pseudometric space, the Hausdorff distance between any set and the empty set is 0.
|
EMetric.infEdist_le_edist_of_mem
theorem EMetric.infEdist_le_edist_of_mem :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s : Set α}, y ∈ s → EMetric.infEdist x s ≤ edist x y := by
sorry
This theorem states that for any type `α` that is a PseudoEMetricSpace (a space where the distance between any two points is defined and always non-negative), for any two points `x` and `y` of that type and for any set `s` of such points, if `y` is a member of `s`, then the minimum extended distance from `x` to the set `s` (denoted as `EMetric.infEdist x s`) is less than or equal to the extended distance from `x` to `y` (denoted as `edist x y`). In other words, the minimum distance from a point to a set is no greater than the distance from the point to any specific member of the set.
More concisely: For any PseudoEMetricSpace `α` and points `x` and `y` in `α` with `y ∈ s`, we have `edist x y ≤ EMetric.infEdist x s`.
|
Metric.exists_dist_lt_of_hausdorffDist_lt
theorem Metric.exists_dist_lt_of_hausdorffDist_lt :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {x : α} {r : ℝ},
x ∈ s → Metric.hausdorffDist s t < r → EMetric.hausdorffEdist s t ≠ ⊤ → ∃ y ∈ t, dist x y < r
This theorem states that given any type `α` equipped with a pseudo metric space structure, and given two sets `s` and `t` of elements of type `α`, if the Hausdorff distance between `s` and `t` is less than a real number `r`, then for any point `x` in set `s`, there is a point `y` in set `t` such that the distance between `x` and `y` is less than `r`. This is under the condition that the Hausdorff edistance between `s` and `t` is not infinity. The Hausdorff distance between two sets here is the smallest nonnegative real number such that each set is included in the 'neighborhood' of the other, and the Hausdorff edistance is the smallest distance such that each set is contained in the 'neighborhood' of the other one.
More concisely: Given a pseudo metric space `(α, d)` and sets `s` and `t` with finite Hausdorff distance, for every `x ∈ s`, there exists `y ∈ t` such that `d(x, y) < r`, where `r` is the Hausdorff distance between `s` and `t`.
|
EMetric.hausdorffEdist_closure₁
theorem EMetric.hausdorffEdist_closure₁ :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
EMetric.hausdorffEdist (closure s) t = EMetric.hausdorffEdist s t
This theorem states that for any two sets `s` and `t` in a pseudo-emetric space `α`, the Hausdorff edistance (or Hausdorff distance) between the closure of `s` and `t` is equal to the Hausdorff edistance between `s` and `t`. In other words, replacing a set `s` with its closure, which is the smallest closed set containing `s`, does not alter the Hausdorff edistance to another set `t`. This edistance is the smallest `r` such that each set is contained in the `r`-neighborhood of the other one.
More concisely: The Hausdorff distance between the closures of sets `s` and `t` in a pseudo-metric space equals the Hausdorff distance between `s` and `t`.
|
EMetric.hausdorffEdist_comm
theorem EMetric.hausdorffEdist_comm :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
EMetric.hausdorffEdist s t = EMetric.hausdorffEdist t s
This theorem, 'EMetric.hausdorffEdist_comm', states that the Hausdorff edistance between two sets 's' and 't' is symmetric. In more detail, for any type 'α' that forms a PseudoEMetricSpace, the Hausdorff edistance from set 's' to 't' is equal to the Hausdorff edistance from set 't' to 's'. The Hausdorff edistance is the smallest 'r' such that each set is contained in the 'r'-neighborhood of the other one.
More concisely: For any sets $s$ and $t$ in a PseudoMetricSpace $\alpha$, the Hausdorff distance between $s$ and $t$ equals the Hausdorff distance between $t$ and $s$.
|
Metric.hausdorffDist_closure₁
theorem Metric.hausdorffDist_closure₁ :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
Metric.hausdorffDist (closure s) t = Metric.hausdorffDist s t
This theorem states that for any two sets `s` and `t` in a pseudo-metric space, the Hausdorff distance between the closure of `s` and `t` is equal to the Hausdorff distance between `s` and `t`. In other words, replacing a set with its closure (the smallest closed set containing it) does not change the Hausdorff distance to any other set. In mathematical terms, if `α` is a type equipped with a pseudo-metric space structure, and `s` and `t` are sets of elements of type `α`, then `Metric.hausdorffDist (closure s) t = Metric.hausdorffDist s t`.
More concisely: In a pseudo-metric space, the Hausdorff distance between the closure of a set and another set is equal to the Hausdorff distance between the original sets.
|