Metric.cthickening_mono
theorem Metric.cthickening_mono :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ₁ δ₂ : ℝ},
δ₁ ≤ δ₂ → ∀ (E : Set α), Metric.cthickening δ₁ E ⊆ Metric.cthickening δ₂ E
The theorem `Metric.cthickening_mono` states that in any pseudo emetric space, the closed δ-thickening of a fixed subset is an increasing function of the thickening radius δ. More specifically, for any two real numbers δ₁ and δ₂ such that δ₁ ≤ δ₂, and for any subset E, the closed δ₁-thickening of E is a subset of the closed δ₂-thickening of E. This essentially means that as we increase the value of δ (the thickening radius), the set of points that are within that distance from E also increases.
More concisely: In any pseudo metric space, the closed δ-thickening of a subset is an increasing function of the radius δ, that is, the closed δ₁-thickening of a subset E is a subset of the closed δ₂-thickening of E for any δ₁ ≤ δ₂.
|
Metric.thickening_mono
theorem Metric.thickening_mono :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ₁ δ₂ : ℝ},
δ₁ ≤ δ₂ → ∀ (E : Set α), Metric.thickening δ₁ E ⊆ Metric.thickening δ₂ E
The theorem `Metric.thickening_mono` states that for any pseudo emetric space `α` and any fixed subset `E` of this space, the thickening of `E` is an increasing function of the thickening radius `δ`. In other words, if `δ₁` and `δ₂` are two real numbers such that `δ₁` is less than or equal to `δ₂`, then the δ₁-thickening of the subset `E` is a subset of the δ₂-thickening of `E`. This is essentially saying that as we increase the radius, the thickening (which consists of points that are at a distance less than the radius from some point of the subset `E`) includes more points.
More concisely: For any pseudo metric space `α` and subset `E`, the thickening function of `E` is monotone increasing with respect to the thickening radius.
|
Metric.closure_eq_iInter_cthickening
theorem Metric.closure_eq_iInter_cthickening :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α), closure E = ⋂ δ, ⋂ (_ : 0 < δ), Metric.cthickening δ E
This theorem states that, in a pseudo emetric space, the closure of a set is equivalent to the intersection of its closed "thickenings" for all positive radii. More intuitively, the closure of a set can be obtained by taking all its closed "thickenings" for any positive radius value, and finding their common elements. A "thickening" of a set here refers to the set of points that lie within a certain distance (the radius) from the original set. The distance is measured using the infimum distance, which is the smallest distance from the point to the set.
More concisely: In a pseudo-metric space, the closure of a set equals the intersection of the closed thickenings of that set for all positive radii.
|
Metric.thickening_eq_biUnion_ball
theorem Metric.thickening_eq_biUnion_ball :
∀ {X : Type u} [inst : PseudoMetricSpace X] {δ : ℝ} {E : Set X}, Metric.thickening δ E = ⋃ x ∈ E, Metric.ball x δ
This theorem states that for any set `E` in a pseudo-metric space (a space where distance between two points is defined), the δ-thickening of `E` (the set of points that are less than δ distance away from any point in `E`) is equivalent to the union of δ-radius balls centered at each point in `E`. In other words, if we take each point in `E` and draw a ball (or sphere) of radius δ around it, the union of all these balls is exactly the δ-thickening of `E`. This theorem holds for any pseudo-metric space `X` and any real number δ.
More concisely: In a pseudo-metric space, the δ-thickening of a set is equal to the union of δ-radius balls centered at each point in the set.
|
Metric.self_subset_thickening
theorem Metric.self_subset_thickening :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ}, 0 < δ → ∀ (E : Set α), E ⊆ Metric.thickening δ E
The theorem states that for any set in a pseudo metric space, the set is contained within its own δ-thickening, given that δ is greater than 0. In other words, every point in the set is within a δ distance from some point in the set. Here, the δ-thickening of a set consists of all points in the space that are less than δ distance away from some point in the set.
More concisely: In a pseudo metric space, every set is contained in its own δ-thickening for any δ > 0. (Every point in the set is within δ distance of some point in the set.)
|
Metric.thickening_singleton
theorem Metric.thickening_singleton :
∀ {X : Type u} [inst : PseudoMetricSpace X] (δ : ℝ) (x : X), Metric.thickening δ {x} = Metric.ball x δ
The theorem `Metric.thickening_singleton` states that for any pseudometric space `X`, any real number `δ`, and any point `x` in `X`, the `δ`-thickening of the singleton set containing only `x` is the same as the metric ball with center `x` and radius `δ`. In simpler terms, it tells us that all the points that are less than `δ` distance away from `x` can be described either as a `δ`-thickening of the set `{x}` or equivalently as a ball of radius `δ` centered at `x`.
More concisely: For any pseudometric space X, point x, and real number δ, the δ-thickening of the singleton set {x} equals the metric ball with center x and radius δ.
|
Metric.self_subset_cthickening
theorem Metric.self_subset_cthickening :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} (E : Set α), E ⊆ Metric.cthickening δ E
This theorem states that, for any set `E` in a pseudo-emetric space `α` and a given real number `δ`, `E` is contained in its own closed `δ`-thickening. In mathematical terms, if `E` is a set in a pseudo-emetric space and `δ` is a real number, then all elements of `E` are also elements of the closed `δ`-thickening of `E`. The closed `δ`-thickening of `E` is the set of all points in the pseudo-emetric space that are at an infimum distance of at most `δ` from `E`.
More concisely: For any set `E` in a pseudo-metric space and real number `δ`, all elements of `E` belong to the closed `δ`-thickening of `E`.
|
Metric.cthickening_eq_iInter_thickening''
theorem Metric.cthickening_eq_iInter_thickening'' :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
Metric.cthickening δ E = ⋂ ε, ⋂ (_ : max 0 δ < ε), Metric.thickening ε E
This theorem states that for any real number `δ` and any set `E` in a pseudo-emetric space `α`, the closed `δ`-thickening of `E` is equivalent to the intersection over all `ε` of the `ε`-thickening of `E`, where `ε` is strictly greater than the maximum of 0 and `δ`.
In other words, it states that the set of points in the space `α` that are at a distance of at most `δ` from the set `E` (the closed δ-thickening) is the same as the set of points that are strictly less than a distance `ε` from `E` for all `ε` greater than the maximum of 0 and `δ`.
More concisely: The closed δ-thickening of a set E in a pseudo-metric space α is equal to the intersection of all (ε-thickening of E) with ε > max(δ, 0).
|
Metric.cthickening_thickening_subset
theorem Metric.cthickening_thickening_subset :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {ε : ℝ},
0 ≤ ε → ∀ (δ : ℝ) (s : Set α), Metric.cthickening ε (Metric.thickening δ s) ⊆ Metric.cthickening (ε + δ) s
This theorem, `Metric.cthickening_thickening_subset`, states that for any pseudo emetric space `α`, any real number `ε` greater than or equal to zero, any real number `δ`, and any subset `s` of `α`, the closed `ε`-thickening of the open `δ`-thickening of `s` is a subset of the closed `(ε + δ)`-thickening of `s`. In other words, it states that for all points within an `ε` distance of some point within a `δ` distance of `s`, they are within an `(ε + δ)` distance of `s`. This theorem involves the concepts of thickening and subset in a pseudo emetric space, which are essential concepts in the study of topology and metric spaces.
More concisely: For any pseudo metric space, the closed ε-thickening of the open δ-thickening of a subset is contained in the closed (ε + δ)-thickening of that subset.
|
Metric.mem_thickening_iff
theorem Metric.mem_thickening_iff :
∀ {δ : ℝ} {X : Type u} [inst : PseudoMetricSpace X] {E : Set X} {x : X},
x ∈ Metric.thickening δ E ↔ ∃ z ∈ E, dist x z < δ
This theorem states that in a pseudometric space, a point `x` belongs to the `δ`-thickening of a subset `E` if and only if there exists some point `z` in `E` such that the distance between `x` and `z` is less than `δ`. The `δ`-thickening of a subset `E` is defined as the collection of points that are less than `δ` distance away from some point in `E`. Here, the distance is measured according to the pseudometric space's distance function.
More concisely: In a pseudometric space, a point belongs to the `δ`-thickening of a subset if and only if there exists a point in the subset with distance less than `δ`.
|
Metric.cthickening_eq_iInter_thickening
theorem Metric.cthickening_eq_iInter_thickening :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ},
0 ≤ δ → ∀ (E : Set α), Metric.cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), Metric.thickening ε E
This theorem states that for any type `α` that has a pseudo emetric space structure, any non-negative real number `δ`, and any set `E` of the type `α`, the closed δ-thickening of `E` is equal to the intersection over all `ε` of the open ε-thickening of `E` for all `ε` larger than `δ`. In other words, the set of all points that are at a distance of at most `δ` from the set `E` is exactly the same as the set of all points that are at a distance less than `ε` from `E` for all `ε` larger than `δ`. This is a statement about how we can construct a closed "thickening" of a set in a pseudo emetric space from open "thickenings".
More concisely: For any pseudo metric space `α` and set `E` in `α`, the closed `δ`-ball around `E` equals the intersection of all open `ε`-balls around `E` with `ε > δ`.
|
Metric.cthickening_eq_iInter_cthickening'
theorem Metric.cthickening_eq_iInter_cthickening' :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ},
∀ s ⊆ Set.Ioi δ,
(∀ (ε : ℝ), δ < ε → (s ∩ Set.Ioc δ ε).Nonempty) →
∀ (E : Set α), Metric.cthickening δ E = ⋂ ε ∈ s, Metric.cthickening ε E
This theorem states that for any type `α` equipped with a pseudo emetric space structure, and for any real number `δ`, if a set `s` is a subset of the interval `(δ, ∞)`, and for any `ε` greater than `δ` the intersection of `s` and the interval `(δ, ε]` is nonempty, then for any set `E` of type `α`, the `δ`-thickening of `E` is equivalent to the intersection over all `ε` in `s` of the `ε`-thickening of `E`. In simpler terms, this theorem essentially describes how the `δ`-thickening of a set `E` can be constructed from all the `ε`-thickenings of `E` for `ε` in a certain subset of `(δ, ∞)`. The term "thickening" in this context refers to the process of enlarging a set by including points that are within a certain distance from the set.
More concisely: For any pseudo metric space `(α, d)` and subset `s` of `(δ, ∞)` such that the intersection of `s` with every `(δ, ε]` is nonempty, the `δ`-thickening of a set `E` is equal to the intersection of the `ε`-thickenings of `E` for all `ε` in `s`.
|
Metric.infEdist_le_infEdist_cthickening_add
theorem Metric.infEdist_le_infEdist_cthickening_add :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α},
EMetric.infEdist x s ≤ EMetric.infEdist x (Metric.cthickening δ s) + ENNReal.ofReal δ
This theorem states that for any pseudo emetric space `α`, a real number `δ`, a set `s` in `α`, and a point `x` in `α`, the infimum edistance (minimum extended distance) from `x` to `s` is less than or equal to the infimum edistance from `x` to the `δ`-thickening of `s` plus `δ`. The `δ`-thickening of a set is defined as the set of points that are at most `δ` away from the original set in the given pseudo emetric space. If `δ` is negative, it is treated as zero by the function `ENNReal.ofReal`. This theorem essentially asserts that enlarging a set by a certain distance increases the minimum distance to a given point by at most that same distance.
More concisely: For any pseudo metric space `α`, point `x` in `α`, set `s` in `α`, and real number `δ`, the infimum distance from `x` to `s` is less than or equal to the infimum distance from `x` to the `δ`-thickening of `s` plus `δ`.
|
Metric.thickening_cthickening_subset
theorem Metric.thickening_cthickening_subset :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} (ε : ℝ),
0 ≤ δ → ∀ (s : Set α), Metric.thickening ε (Metric.cthickening δ s) ⊆ Metric.thickening (ε + δ) s
This theorem, `Metric.thickening_cthickening_subset`, states that for any type `α` that forms a pseudo emetric space, any non-negative real number `δ`, any real number `ε`, and any subset `s` of `α`, the `ε`-thickening of the `δ`-closed thickening of `s` is contained within the `(ε + δ)`-thickening of `s`. In other words, if we first apply a `δ`-closed thickening operation to a set `s` and then apply an `ε`-thickening operation to the result, all the points obtained will be within a `(ε + δ)`-thickening of the original set `s`.
More concisely: For any pseudo metric space (α, d), real numbers δ ≥ 0 and ε ≥ 0, and subset s of α, the ε-thickening of the δ-closed thickening of s is included in the (ε + δ)-thickening of s.
|
Metric.closure_subset_thickening
theorem Metric.closure_subset_thickening :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ}, 0 < δ → ∀ (E : Set α), closure E ⊆ Metric.thickening δ E := by
sorry
This theorem states that, for any given type `α` that is a pseudo emetric space, for any real number `δ` that is greater than zero, and for any set `E` of type `α`, the closure of `E` is a subset of the `δ`-thickening of `E`. In other words, all the points in the topological closure of a set `E` are included within the open `δ`-thickening of `E`, which consists of points that are at a distance less than `δ` from some point of `E`.
More concisely: For any pseudo metric space `α` and `δ` > 0, the closure of a set `E` in `α` is contained in the `δ`-thickening of `E`.
|
Metric.eventually_not_mem_cthickening_of_infEdist_pos
theorem Metric.eventually_not_mem_cthickening_of_infEdist_pos :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {E : Set α} {x : α},
x ∉ closure E → ∀ᶠ (δ : ℝ) in nhds 0, x ∉ Metric.cthickening δ E
The theorem `Metric.eventually_not_mem_cthickening_of_infEdist_pos` states that for any point `x` which is exterior to a subset `E` (meaning `x` is outside the closure of `E`) in a pseudo emetric space, there exists a small enough positive real number `δ` such that `x` is not in the closed `δ`-thickening of `E`. The closed `δ`-thickening of a subset `E` is the set of points that are at a distance of at most `δ` from `E`. The 'small enough' `δ` is described as being eventually in the neighborhood of 0, which means that all sufficiently small positive real numbers in a neighborhood around 0 will satisfy the condition that `x` is not in the closed `δ`-thickening of `E`.
More concisely: For any point exterior to a subset in a pseudo metric space, there exists a positive real number δ such that the closed δ-thickening of the subset does not contain the point.
|
Metric.isClosed_cthickening
theorem Metric.isClosed_cthickening :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {E : Set α}, IsClosed (Metric.cthickening δ E)
This theorem states that in any pseudo emetric space, the closed δ-thickening of a subset is a closed set. To elaborate, given a subset E of some type α, where α boasts a pseudo emetric space structure, and a real number δ, the "closed δ-thickening" of E is always a closed set. Here, the "closed δ-thickening" of E, denoted as `Metric.cthickening δ E`, refers to the collection of points in α that are at an infimum (or minimum) distance of at most δ from the subset E.
More concisely: In any pseudo metric space, the closed δ-thickening of a subset is a closed set. That is, `Metric.cthickening δ E` is a closed subset of the space for any subset `E` and real number `δ`.
|
IsCompact.cthickening_eq_biUnion_closedBall
theorem IsCompact.cthickening_eq_biUnion_closedBall :
∀ {α : Type u_2} [inst : PseudoMetricSpace α] {δ : ℝ} {E : Set α},
IsCompact E → 0 ≤ δ → Metric.cthickening δ E = ⋃ x ∈ E, Metric.closedBall x δ
This theorem states that for a given compact set `E` in a pseudo-metric space `α`, the `δ`-thickening of `E` is equivalent to the union of all closed balls of radius `δ` centered at each point `x` in `E`. In other words, it means that each point in the `δ`-thickening of `E` is within `δ` distance of some point in `E`, and this point is the center of one of the closed balls included in the union. The theorem also requires that `δ` must be a non-negative real number.
More concisely: For a compact set `E` in a pseudo-metric space `α` and a non-negative real number `δ`, the `δ`-thickening of `E` is equal to the union of all closed balls of radius `δ` centered at points in `E`.
|
Metric.thickening_of_nonpos
theorem Metric.thickening_of_nonpos :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ}, δ ≤ 0 → ∀ (s : Set α), Metric.thickening δ s = ∅
The theorem `Metric.thickening_of_nonpos` states that in any pseudo emetric space, the δ-thickening of a set is empty if δ is less than or equal to zero. In simpler terms, if we try to create a set of points that are less than or equal to zero distance from a given set (which makes little sense as distances are non-negative), we end up with no points, or an empty set.
More concisely: In a pseudo metric space, the δ-thickening of a set is empty for δ ≤ 0.
|
Metric.thickening_eq_preimage_infEdist
theorem Metric.thickening_eq_preimage_infEdist :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
Metric.thickening δ E = (fun x => EMetric.infEdist x E) ⁻¹' Set.Iio (ENNReal.ofReal δ)
This theorem states that, in any pseudo emetric space, the open δ-thickening of a subset E is equivalent to the preimage of an open interval under the function mapping a point to its minimal edistance to the set E. In other words, the δ-thickening of a set is comprised of all points whose minimum extended distance to the set is less than δ. The open interval is formed using the function `ENNReal.ofReal δ` which returns δ if it is nonnegative, and `0` otherwise.
More concisely: In a pseudometric space, the open δ-thickening of a set equals the preimage of the open interval (0, min distance function(x, E) + δ) under the function mapping a point to its minimum distance to the set E.
|
Metric.thickening_subset_cthickening
theorem Metric.thickening_subset_cthickening :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α), Metric.thickening δ E ⊆ Metric.cthickening δ E
The theorem `Metric.thickening_subset_cthickening` states that for any set `E` of points in a pseudo-emetric space (a space endowed with a distance function satisfying certain properties), the open $\delta$-thickening of `E` (which is the set of all points less than $\delta$ away from any point in `E`) is a subset of the closed $\delta$-thickening of `E` (which is the set of all points whose distance to `E` is at most $\delta$). This implies that any point that is less than $\delta$ away from some point of `E` will also be at most $\delta$ away from `E`.
More concisely: The open thickening of a set in a pseudo-metric space is contained in its closed thickening.
|
Metric.cthickening_subset_thickening'
theorem Metric.cthickening_subset_thickening' :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ₁ δ₂ : ℝ},
0 < δ₂ → δ₁ < δ₂ → ∀ (E : Set α), Metric.cthickening δ₁ E ⊆ Metric.thickening δ₂ E
The theorem `Metric.cthickening_subset_thickening'` states that for any subset `E` of a pseudo emetric space, the closed thickening of `E` with a radius `δ₁`, denoted `Metric.cthickening δ₁ E`, is a subset of the open thickening of `E` with a radius `δ₂`, denoted `Metric.thickening δ₂ E`, if `δ₂` is positive and larger than `δ₁`.
Here, a closed thickening of a set `E` consists of points that are at a distance at most `δ₁` from `E` and an open thickening of `E` consists of points that are at a distance less than `δ₂` from some point in `E`.
More concisely: For any subset `E` of a pseudo metric space, the closed thickening of `E` with radius `δ₁` is contained in the open thickening of `E` with radius `δ₂` when `δ₂` is positive and larger than `δ₁`.
|
Metric.closure_eq_iInter_cthickening'
theorem Metric.closure_eq_iInter_cthickening' :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α) (s : Set ℝ),
(∀ (ε : ℝ), 0 < ε → (s ∩ Set.Ioc 0 ε).Nonempty) → closure E = ⋂ δ ∈ s, Metric.cthickening δ E
The theorem `Metric.closure_eq_iInter_cthickening'` states that, for any set `E` in a PseudoEMetricSpace `α` and any set of real numbers `s`, if for every positive real number `ε`, the intersection of `s` and the interval `(0, ε]` is nonempty (i.e., there are numbers in `s` within any positive distance from zero), then the closure of `E` is the intersection of the closed `δ`-thickenings of `E` for each `δ` in `s`. In simpler terms, the closure of a set can be obtained by intersecting all closed thickenings of the set with thickness ranging over any set of positive real numbers that accumulate at zero.
More concisely: For any PseudoEMetricSpace `α` and set `E` in it, if for every positive real number `ε`, the set `s` intersects the open interval `(0, ε] non-empty, then the closure of `E` equals the intersection of the closed `δ`-thickenings of `E` for all `δ` in `s`.
|
Metric.closedBall_subset_cthickening
theorem Metric.closedBall_subset_cthickening :
∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {E : Set α},
x ∈ E → ∀ (δ : ℝ), Metric.closedBall x δ ⊆ Metric.cthickening δ E
The theorem `Metric.closedBall_subset_cthickening` states that for any type `α` with a `PseudoMetricSpace` structure, any point `x` from a set `E` and any real number `δ`, the closed ball of radius `δ` centered at `x` is a subset of the closed δ-thickening of `E`. In other words, every point that lies within the closed ball, which includes all points with distance from `x` less than or equal to `δ`, also lies within the closed δ-thickening of `E`, a set which includes all points whose minimum distance from `E` is less than or equal to `δ`.
More concisely: For any pseudo-metric space (α, d), and point x in α and real number δ, the closed ball B(x, δ) is contained in the closed δ-thickening Thick(E, δ) of any set E in α.
|
Metric.cthickening_singleton
theorem Metric.cthickening_singleton :
∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x : α) {δ : ℝ},
0 ≤ δ → Metric.cthickening δ {x} = Metric.closedBall x δ
The theorem `Metric.cthickening_singleton` states that for any type `α` equipped with a pseudo metric space structure, and for any element `x` of type `α` and any real number `δ` greater than or equal to zero, the closed `δ`-thickening of the set containing only `x` is equal to the closed ball centered at `x` with radius `δ`. In other words, the set of all points at an infimum distance of at most `δ` from `x` is the same as the set of all points whose distance from `x` is at most `δ`.
More concisely: For any pseudo metric space `(α, d)` and `x ∈ α` with real `δ ≥ 0`, the closed `δ`-thickening of the singleton set `{x}` equals the closed ball `{y | d(x, y) ≤ δ}`.
|
Metric.thickening_subset_of_subset
theorem Metric.thickening_subset_of_subset :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) {E₁ E₂ : Set α},
E₁ ⊆ E₂ → Metric.thickening δ E₁ ⊆ Metric.thickening δ E₂
The theorem `Metric.thickening_subset_of_subset` states that for any two subsets `E₁` and `E₂` of a given pseudo emetric space `α`, if `E₁` is a subset of `E₂`, then the `δ`-thickening of `E₁` is also a subset of the `δ`-thickening of `E₂`. Here, the `δ`-thickening of a set `E` refers to the set of all points in the space that are at a distance less than `δ` from some point in `E`. This theorem essentially implies that the operation of thickening a set by a fixed radius `δ` preserves the subset relation.
More concisely: Given any pseudo metric space α and subsets E₁, E₂ with E₁ ⊆ E₂, the δ-thickening of E₁ is contained in the δ-thickening of E₂.
|
Metric.cthickening_cthickening_subset
theorem Metric.cthickening_cthickening_subset :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ ε : ℝ},
0 ≤ ε → 0 ≤ δ → ∀ (s : Set α), Metric.cthickening ε (Metric.cthickening δ s) ⊆ Metric.cthickening (ε + δ) s
The theorem `Metric.cthickening_cthickening_subset` states that for any type `α` that is a pseudo emetric space, any non-negative real numbers `ε` and `δ`, and any set `s` of type `α`, the `ε`-thickening of the `δ`-thickening of `s` is a subset of the `(ε + δ)`-thickening of `s`. In other words, if you first thicken the set `s` by `δ` and then thicken the result by `ε`, any point in the final set is also in the set obtained by thickening `s` directly by `(ε + δ)`. This provides a relationship between the operation of thickening a set in a pseudo emetric space and the addition of real numbers.
More concisely: For any pseudo metric space `(α, d)`, and sets `s ⊆ α` and `ε, δ ∈ ℝ^+`, the `(ε + δ)`-thickening of `s` contains the `ε`-thickening of the `δ`-thickening of `s`.
|
Metric.infEdist_le_infEdist_thickening_add
theorem Metric.infEdist_le_infEdist_thickening_add :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α},
EMetric.infEdist x s ≤ EMetric.infEdist x (Metric.thickening δ s) + ENNReal.ofReal δ
This theorem states that for any pseudo emetric space `α`, a real number `δ`, a set `s` in `α`, and a point `x` in `α`, the minimal extended distance from `x` to the set `s` is less than or equal to the minimal extended distance from `x` to the `δ`-thickening of the set `s` plus `δ`. Here, the `δ`-thickening of a set `s` refers to the collection of points in `α` that are less than `δ` away from any point in `s`. The function `ENNReal.ofReal` returns `δ` if it is nonnegative, `0` otherwise.
More concisely: For any pseudo metric space `α`, point `x` in `α`, set `s` in `α`, and real number `δ ≥ 0`, the minimal extended distance from `x` to `s` is less than or equal to the minimal extended distance from `x` to the `δ`-thickening of `s` plus `δ`.
|
Bornology.IsBounded.cthickening
theorem Bornology.IsBounded.cthickening :
∀ {α : Type u_2} [inst : PseudoMetricSpace α] {δ : ℝ} {E : Set α},
Bornology.IsBounded E → Bornology.IsBounded (Metric.cthickening δ E)
The theorem `Bornology.IsBounded.cthickening` states that for any type `α` that is a pseudo metric space, any real number `δ`, and any set `E` of type `α`, if `E` is a bounded set (in the sense of the ambient bornology on `α`), then the `δ`-thickening of `E` is also a bounded set. In this context, the `δ`-thickening of a set `E` consists of those points that are at most `δ` away from `E` in terms of the infimum distance.
More concisely: For any bounded set `E` in a pseudo metric space `α`, the `δ-`thickening of `E` is also a bounded set.
|
Metric.thickening_thickening_subset
theorem Metric.thickening_thickening_subset :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (ε δ : ℝ) (s : Set α),
Metric.thickening ε (Metric.thickening δ s) ⊆ Metric.thickening (ε + δ) s
The theorem `Metric.thickening_thickening_subset` states that for any pseudo emetric space `α`, real numbers `ε` and `δ`, and a given set `s` of type `α`, the `ε`-thickening of the `δ`-thickening of `s` is a subset of the `(ε + δ)`-thickening of `s`. In other words, for every point which lies within a distance `ε` from any point that lies within a distance `δ` from `s`, that point also lies within a distance `(ε + δ)` from `s`.
More concisely: For any pseudo metric space `α`, sets `s` of type `α`, and real numbers `ε ≥ 0` and `δ ≥ 0`, the `(ε + δ)`-neighborhood of `s` contains the `ε`-neighborhood of the `δ`-neighborhood of `s`.
|
Metric.frontier_thickening_subset
theorem Metric.frontier_thickening_subset :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α) {δ : ℝ},
frontier (Metric.thickening δ E) ⊆ {x | EMetric.infEdist x E = ENNReal.ofReal δ}
The theorem `Metric.frontier_thickening_subset` states that for any set `E` in a pseudo emetric space `α`, and any real number `δ`, the frontier of the `δ`-thickening of `E` is a subset of the set of points where the infimum extended metric distance to `E` equals `δ`. In less formal terms, this means that the boundary of the region containing points that are less than a certain distance `δ` from `E`, is included within the set of points that are exactly `δ` distance away from `E`.
More concisely: The frontier of the `δ`-thickening of a set `E` in a pseudo metric space is contained in the set of points with exact distance `δ` to `E`.
|
Metric.cthickening_of_nonpos
theorem Metric.cthickening_of_nonpos :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ}, δ ≤ 0 → ∀ (E : Set α), Metric.cthickening δ E = closure E
This theorem states that for any type `α` equipped with a `PseudoEMetricSpace` structure, and for a real number `δ` that is less than or equal to zero and any set `E` of this type `α`, the `δ`-thickening of `E` (denoted as `Metric.cthickening δ E`) is equal to the closure of `E`. In other words, if we consider all points that are at most `δ` away from `E` in terms of the pseudo emetric (where `δ` is nonpositive), we end up with the smallest closed set that contains `E`, which is the definition of the closure of `E`.
More concisely: For any `PseudoEMetricSpace` `α` and `δ ≤ 0`, the `δ`-thickening of a set `E` in `α` equals the closure of `E`.
|
Metric.cthickening_subset_of_subset
theorem Metric.cthickening_subset_of_subset :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) {E₁ E₂ : Set α},
E₁ ⊆ E₂ → Metric.cthickening δ E₁ ⊆ Metric.cthickening δ E₂
The theorem `Metric.cthickening_subset_of_subset` states that in any pseudo emetric space, if `E₁` is a subset of `E₂`, then the δ-thickened set of `E₁` is also a subset of the δ-thickened set of `E₂`. Here, δ-thickening (denoted as `Metric.cthickening δ E`) of a set `E` is defined as those points that are at an infimum distance at most `δ` from `E`. This theorem essentially says that increasing the subset `E` in the δ-thickening operation results in an increase of the thickened set.
More concisely: In a pseudo metric space, the δ-thickening of a subset is monotonic with respect to subset inclusion. That is, if E₁ ⊆ E₂, then Metric.cthickening δ E₁ ⊆ Metric.cthickening δ E₂.
|
Metric.closure_subset_cthickening
theorem Metric.closure_subset_cthickening :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α), closure E ⊆ Metric.cthickening δ E
This theorem states that for every set `E` in a pseudo emetric space of type `α`, the closure of `E` is a subset of the closed `δ`-thickening of `E`. In other words, every point that belongs to the closure of `E` will be contained in the set of points that are at infimum distance at most `δ` from `E`. Here, the closure of `E` represents the smallest closed set that contains `E`, and the `δ`-thickening of `E` represents the set of points that are within a certain distance `δ` from `E`.
More concisely: For every pseudo metric space `α` and set `E` in it, the closure of `E` is contained in the `δ`-thickening of `E`.
|
Metric.cthickening_zero
theorem Metric.cthickening_zero :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α), Metric.cthickening 0 E = closure E
This theorem states that, in any pseudo emetric space, the closed thickening of a set at radius zero is equivalent to the closure of the set. In other words, the set of all points that are at an infimum distance of zero from the set is the same as the smallest closed set containing the said set. This theorem holds for all sets in any pseudo emetric space.
More concisely: In a pseudo metric space, the closed thickening of a set at radius 0 is equal to its closure.
|
Metric.frontier_cthickening_subset
theorem Metric.frontier_cthickening_subset :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α) {δ : ℝ},
frontier (Metric.cthickening δ E) ⊆ {x | EMetric.infEdist x E = ENNReal.ofReal δ}
The theorem `Metric.frontier_cthickening_subset` states that for any set `E` in a pseudo emetric space `α` and any real number `δ`, the frontier (the points between the closure and the interior) of the closed `δ`-thickening of `E` is a subset of the set of points whose minimum extended metric distance to `E` equals `δ`. The closed `δ`-thickening of a set `E` consists of those points that are at the infimum distance at most `δ` from `E`.
More concisely: The theorem asserts that the frontier of the closed δ-thickening of a set E in a pseudo metric space equals the set of points with minimum extended metric distance to E equal to δ.
|
Mathlib.Topology.MetricSpace.Thickening._auxLemma.3
theorem Mathlib.Topology.MetricSpace.Thickening._auxLemma.3 :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} (E : Set α) (x : α),
(x ∈ Metric.thickening δ E) = ∃ z ∈ E, edist x z < ENNReal.ofReal δ
The theorem `Mathlib.Topology.MetricSpace.Thickening._auxLemma.3` states that for any type `α` endowed with the structure of a pseudo emetric space, any real number `δ`, any set `E` of elements of type `α`, and any element `x` of type `α`, the membership of `x` in the `δ`-thickening of `E` (i.e., the set of points at a distance less than `δ` from some point in `E`) is equivalent to the existence of an element `z` in `E` such that the extended distance between `x` and `z` is less than the non-negative real part of `δ`.
More concisely: For any pseudo metric space (α, d), real number δ, set E ⊆ α, and x ∈ α, x is in the δ-thickening of E if and only if there exists z ∈ E such that d(x, z) < ∥δ∥.
|
Metric.thickening_empty
theorem Metric.thickening_empty : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ), Metric.thickening δ ∅ = ∅ := by
sorry
This theorem states that the open thickening of the empty set is itself an empty set for any pseudo emetric space. In other words, if we consider any pseudo emetric space and attempt to create a "δ-thickening" of the empty set (a set of points that are less than distance δ from any point in the empty set), the result will always be the empty set, regardless of the value of δ.
More concisely: For any pseudo metric space, the open δ-ball around the empty set is empty for all δ ≥ 0.
|
Metric.cthickening_empty
theorem Metric.cthickening_empty : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ), Metric.cthickening δ ∅ = ∅
The theorem `Metric.cthickening_empty` states that in any pseudo emetric space, the closed δ-thickening of an empty set is also an empty set, regardless of the value of δ. In other words, there are no points within a δ distance from an empty set.
More concisely: In any pseudo metric space, the closed δ-thickening of the empty set is empty for all δ ≥ 0.
|
Metric.closure_eq_iInter_thickening
theorem Metric.closure_eq_iInter_thickening :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α), closure E = ⋂ δ, ⋂ (_ : 0 < δ), Metric.thickening δ E
The theorem `Metric.closure_eq_iInter_thickening` states that for any set `E` in a pseudo emetric space `α`, the closure of `E` is equal to the intersection of all its open thickenings of positive radii. In other words, the smallest closed set containing `E` is equivalent to the intersection of sets of points that are less than any positive real number distance (`δ`) away from some point in `E`.
More concisely: The closure of a set in a pseudometric space equals the intersection of all open thickenings of positive radii around points in the set.
|
IsCompact.exists_cthickening_subset_open
theorem IsCompact.exists_cthickening_subset_open :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
IsCompact s → IsOpen t → s ⊆ t → ∃ δ, 0 < δ ∧ Metric.cthickening δ s ⊆ t
This theorem states that if we have a subset `s` of a given type `α` in a pseudo emetric space, and `s` is compact, and if `t` is another subset of the same type `α` which is an open set, and `s` is contained in `t`, then we can find a positive real number `δ` such that the δ-thickening of `s` is still contained within `t`. Here, δ-thickening of `s` refers to the set of all points in the pseudo emetric space that are at an infimum distance of `δ` or less from `s`.
More concisely: If `s` is a compact subset of a pseudo metric space `α`, `t` is an open set containing `s`, then there exists a real number `δ > 0` such that the `δ`-thickening of `s` (the set of points within infimum distance `δ` of `s`) is contained in `t`.
|
Mathlib.Topology.MetricSpace.Thickening._auxLemma.8
theorem Mathlib.Topology.MetricSpace.Thickening._auxLemma.8 :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α},
(x ∈ Metric.cthickening δ s) = (EMetric.infEdist x s ≤ ENNReal.ofReal δ)
This theorem, `Mathlib.Topology.MetricSpace.Thickening._auxLemma.8`, is a statement about the relationship between a point and a certain set in a pseudo emetric space. Specifically, for any pseudo metric space `α`, any real number `δ`, any set `s` of type `α`, and any point `x` of type `α`, the theorem establishes that the point `x` is in the `δ`-thickening of the set `s` if and only if the infimum extended distance from the point `x` to the set `s` is less than or equal to the extended non-negative real representation of `δ`. In other words, it connects the concept of a `δ`-thickening of a set (which includes all points within a certain "thickness" or distance from the set) with the concept of the infimum extended distance of a point from a set.
More concisely: In a pseudo metric space, a point is in the `δ`-thickening of a set if and only if the infimum extended distance from the point to the set is less than or equal to the extended non-negative real representation of `δ`.
|
Metric.eventually_not_mem_thickening_of_infEdist_pos
theorem Metric.eventually_not_mem_thickening_of_infEdist_pos :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {E : Set α} {x : α},
x ∉ closure E → ∀ᶠ (δ : ℝ) in nhds 0, x ∉ Metric.thickening δ E
This theorem states that for any point `x` in a pseudo-emetric space `α` that is an exterior point of a given set `E` (meaning `x` is not contained in the closure of `E`), there exists a small enough positive real number `δ` such that `x` is not within the `δ`-thickening of `E`. Here, the `δ`-thickening of `E` is defined as the set of all points within `δ` distance from any point in `E`, and `nhds 0` is the set of neighborhoods of 0, which in this case is used to describe the concept of "small enough positive numbers". The statement "∀ᶠ" is read as "for all eventually", meaning that the condition holds for all elements beyond a certain point in the set.
More concisely: For any exterior point `x` in a pseudo-metric space `α` and set `E`, there exists a positive real number `δ` such that `x` is not contained in the `δ`-thickening of `E` (i.e., `x` is not in the closure of `E`).
|
Mathlib.Topology.MetricSpace.Thickening._auxLemma.13
theorem Mathlib.Topology.MetricSpace.Thickening._auxLemma.13 : ∀ {α : Type u} (s : Set α), (∅ ⊆ s) = True
This theorem, named as `Mathlib.Topology.MetricSpace.Thickening._auxLemma.13`, states that for any type `α` and any set `s` of type `α`, the empty set is always a subset of `s`. This fact is universally true, hence the output is `True`. In mathematical terms, we can express this as for all sets `s`, the relation `∅ ⊆ s` is always satisfied.
More concisely: The empty set is a subset of any set.
|
Metric.isOpen_thickening
theorem Metric.isOpen_thickening :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {E : Set α}, IsOpen (Metric.thickening δ E)
The theorem `Metric.isOpen_thickening` states that for any type `α` which has an instance of a `PseudoEMetricSpace`, and any real number `δ` and set `E`, the `δ`-thickening of `E` is an open set. In mathematical terms, the `δ`-thickening of a set `E` in a pseudo emetric space, denoted as `Metric.thickening δ E`, is the set of points that are at a distance less than `δ` from any point in `E`. This theorem guarantees that such a `δ`-thickening of a set `E` is an open set in the topology induced by this pseudo emetric space.
More concisely: In a pseudo metric space, the δ-thickening of a set is an open set.
|
Metric.closure_eq_iInter_thickening'
theorem Metric.closure_eq_iInter_thickening' :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α),
∀ s ⊆ Set.Ioi 0, (∀ (ε : ℝ), 0 < ε → (s ∩ Set.Ioc 0 ε).Nonempty) → closure E = ⋂ δ ∈ s, Metric.thickening δ E
The theorem `Metric.closure_eq_iInter_thickening'` states that for every set `E` in a pseudo emetric space `α`, the closure of the set `E` is equivalent to the intersection of open thickenings of `E` with positive radii accumulating at zero. More concretely, given any subset `s` of the left-open right-infinite interval `(0, ∞)`, if for any real number `ε` greater than zero, there exists a nonempty intersection between `s` and the left-open right-closed interval `(0, ε)`, then the closure of `E` is the same as the intersection of the `δ`-thickening of `E` for all `δ` in `s`. In terms of metric spaces, this theorem is expressing that the closure of a set can be thought of as the accumulation of all the points that are arbitrarily close to the set.
More concisely: Given a pseudo metric space and a set E, the closure of E equals the intersection of the open thickenings of E with radii in the set of positive real numbers accumulating at zero.
|