inv_closedBall
theorem inv_closedBall :
∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E),
(Metric.closedBall x δ)⁻¹ = Metric.closedBall x⁻¹ δ
The theorem `inv_closedBall` states that for any type `E` that is a semi-normed commutative group, any real number `δ`, and any element `x` of `E`, the inverse of the closed ball centered at `x` with radius `δ` is equal to the closed ball centered at the inverse of `x` with radius `δ`. In other words, if you take the set of all points whose distance from `x` is less than or equal to `δ`, and then take the inverse of all those points, you end up with the same set as if you had started with the inverse of `x` and taken the set of all points whose distance from the inverse of `x` is less than or equal to `δ`.
More concisely: For any semi-normed commutative group `E` and real number `δ`, the inverse of the closed ball `{x : E | norm x ≤ δ} around `x` is equal to the closed ball `{y : E | norm (inv x) ≤ δ} around the additive inverse `inv x` of `x`.
|
vadd_closedBall_zero
theorem vadd_closedBall_zero :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E),
x +ᵥ Metric.closedBall 0 δ = Metric.closedBall x δ
The theorem `vadd_closedBall_zero` states that for any type `E` that forms a semi-normed addition-commutative group, and for any real number `δ` and element `x` of `E`, adding `x` to every element in the closed ball (the set of all points `y` with distance from `y` to the origin `0` less than or equal to `δ`) gives the closed ball centered at `x` with radius `δ`. In other words, translating the origin-centered closed ball by `x` results in the closed ball centered at `x`.
More concisely: For any semi-normed addition-commutative group `E` and real number `δ`, the set of elements with distance less than or equal to `δ` from `x` is equal to the set of elements with distance less than or equal to `δ` from `0` translated by `x`.
|
singleton_add_closedBall
theorem singleton_add_closedBall :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E),
{x} + Metric.closedBall y δ = Metric.closedBall (x + y) δ
The theorem `singleton_add_closedBall` states that for any type `E` which is a seminormed additive commutative group, any real number `δ`, and any two elements `x` and `y` of `E`, the set obtained by adding the singleton set containing `x` to the closed ball centered at `y` with radius `δ` (which is the set of all points in `E` whose distance to `y` is less than or equal to `δ`) is equal to the closed ball centered at `x + y` with radius `δ`. In other words, translating the entire ball by `x` in the seminormed additive commutative group `E` gives the same set as the ball centered at `x + y`.
More concisely: For any seminormed additive commutative group `E`, real number `δ`, and elements `x, y` in `E`, the closed ball centered at `x + y` with radius `δ` equals the set obtained by translating the closed ball centered at `y` with radius `δ` by adding `x`.
|
neg_ball
theorem neg_ball :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), -Metric.ball x δ = Metric.ball (-x) δ := by
sorry
The theorem `neg_ball` states that for all types `E` that form a seminormed additive commutative group, and for any real number `δ` and any element `x` of `E`, the negation of the set of all points `y` where the distance between `y` and `x` is less than `δ` (`-Metric.ball x δ`) is equal to the set of all points `y` where the distance between `y` and the negation of `x` (`-x`) is less than `δ` (`Metric.ball (-x) δ`). This suggests an element-wise negation symmetry in the metric space around the origin.
More concisely: For any seminormed additive commutative group `E` and real number `δ`, `-Metric.ball x δ = Metric.ball (-x) δ`.
|
neg_closedBall
theorem neg_closedBall :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E),
-Metric.closedBall x δ = Metric.closedBall (-x) δ
This theorem states that for any seminormed additive commutative group `E` and any real number `δ`, the negation of the closed ball around a point `x` in `E` with radius `δ` is equal to the closed ball around the negation of `x` with the same radius `δ`. In other words, reflecting the set of all points in the group that are within a distance `δ` from `x` around the origin yields the same set of points as those that are within a distance `δ` from `-x`.
More concisely: For any seminormed additive commutative group `E` and real number `δ`, the negative of the closed ball around `x` in `E` with radius `δ` is equal to the closed ball around `-x`.
|
IsCompact.add_closedBall
theorem IsCompact.add_closedBall :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
IsCompact s → 0 ≤ δ → ∀ (x : E), s + Metric.closedBall x δ = x +ᵥ Metric.cthickening δ s
The theorem `IsCompact.add_closedBall` states that for any seminormed additive commutative group `E`, nonnegative real number `δ`, and a set `s` of type `E` that is compact, for any element `x` in `E`, the sum of set `s` and the closed ball centered at `x` with radius `δ` equals the sum of `x` and the `δ`-thickening of set `s`. Here, the sum of a set and a closed ball refers to the set of all sums of an element from the set and an element from the closed ball, and similarly for the sum of a point `x` and a set. The `δ`-thickening of a set `s` consists of points whose minimum distance from `s` is at most `δ`.
More concisely: For any compact set $s$ in a seminormed additive commutative group $E$ and any element $x$ in $E$, the sum of $s$ and the closed ball centered at $x$ with radius $\delta$ equals the set of all sums of an element from $s$ and an element from the $\delta$-thickening of $x$ around $s$.
|
inv_ball
theorem inv_ball :
∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), (Metric.ball x δ)⁻¹ = Metric.ball x⁻¹ δ
The theorem `inv_ball` states that for every seminormed commutative group `E` of type `u_1`, and for every real number `δ` and element `x` of `E`, the inverse of the metric ball centered at `x` with radius `δ` is equal to the metric ball centered at the inverse of `x` with radius `δ`. In other words, inverting the elements of a metric ball does not change the metric ball itself.
More concisely: For every seminormed commutative group `E` and real number `δ`, the inverse of the metric ball `{x : E | dist x x_0 < δ}` centered at `x_0` is equal to the metric ball `{x : E | dist x x_0^(-1) < δ}` centered at the inverse of `x_0` in `E`.
|
add_ball_zero
theorem add_ball_zero :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E),
s + Metric.ball 0 δ = Metric.thickening δ s
This theorem states that for any set `s` of elements in a seminormed additive commutative group `E` and a real number `δ`, the sum of `s` and the set of all points `y` such that the distance from `y` to the origin (`0`) is less than `δ` (`Metric.ball 0 δ`) is equal to the δ-thickening of `s` (`Metric.thickening δ s`). In other words, the set of points resulting from the element-wise addition of `s` and the open ball of radius `δ` centered at the origin is exactly the same as the set of all points that are at a distance less than `δ` from any point in `s`.
More concisely: For any seminormed additive commutative group `E` with metric `Metric`, set `s ∈ E`, and real number `δ > 0`, the set `s + Metric.ball δ 0` equals `Metric.thickening δ s`.
|
ball_add
theorem ball_add :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E),
Metric.ball x δ + s = x +ᵥ Metric.thickening δ s
This theorem states that for any seminormed additive commutative group `E`, real number `δ`, set `s` of type `E`, and element `x` of type `E`, the addition of the open ball of radius `δ` centered at `x` and the set `s` is equal to the addition of `x` and the `δ`-thickening of the set `s`. In mathematical terms, if `s` is a set in `E`, `x` is an element of `E`, and `δ` is a real number, then the set of all points within distance `δ` from `x` added to `s` is the same as the set of all points `x` plus those points in `E` that are less than `δ` away from any point in `s`.
More concisely: For any seminormed additive commutative group `E`, real number `δ`, and set `s` in `E`, the set `{x + y : x ∈ E, y ∈ s, ∥y∥ < δ}` is equal to `{z : ∥z - x∥ < δ, z ∈ s}`.
|
singleton_mul_closedBall
theorem singleton_mul_closedBall :
∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E),
{x} * Metric.closedBall y δ = Metric.closedBall (x * y) δ
This theorem, `singleton_mul_closedBall`, states that for any type `E` which has an instance of a `SeminormedCommGroup`, any real number `δ`, and any two elements `x` and `y` of `E`, the set multiplication of the singleton set `{x}` and the closed ball centered at `y` with radius `δ` (which is the set of all points at a distance `≤ δ` from `y`) is equal to the closed ball centered at `x * y` with radius `δ`. In other words, scaling and shifting the points within the `δ`-radius ball around `y` by a factor of `x` gives us the same set of points as in the `δ`-radius ball around `x * y`.
More concisely: For any type `E` with a `SeminormedCommGroup` instance, and for all `x`, `y` in `E` and `δ` in `ℝ`, the set `{x} * ℯ_(δ)(y)` equals `ℯ_(δ)(x * y)`, where `ℯ_(δ)` denotes the closed ball with radius `δ` around a point.
|
IsCompact.mul_closedBall_one
theorem IsCompact.mul_closedBall_one :
∀ {E : Type u_1} [inst : SeminormedCommGroup E] {δ : ℝ} {s : Set E},
IsCompact s → 0 ≤ δ → s * Metric.closedBall 1 δ = Metric.cthickening δ s
This theorem states that for any set `s` of elements from a seminormed commutative group `E`, given a non-negative real number `δ`, if `s` is a compact set, then the product of `s` and the closed ball centered at `1` with radius `δ`, which consists of all the points in `E` whose distance from `1` is less than or equal to `δ`, is exactly the closed `δ`-thickening of `s`. Here, the closed `δ`-thickening of `s` is defined as the set of all points in `E` that are at most `δ` away from `s` in terms of the infimum extended metric distance.
More concisely: For a compact set `s` in a seminormed commutative group `E` and a non-negative real number `δ`, the product of `s` and the closed ball with radius `δ` centered at `1` equals the closed `δ`-thickening of `s` in terms of the infimum extended metric distance.
|
ball_add_zero
theorem ball_add_zero :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E),
Metric.ball 0 δ + s = Metric.thickening δ s
This theorem, `ball_add_zero`, states that for any subset `s` of a seminormed additive commutative group `E` and any real number `δ`, the sum of the ball of radius `δ` centered at the origin and the set `s` is equal to the `δ`-thickening of the set `s`. In other words, the set of all points within a distance `δ` from the origin plus any element in `s` is the same as the set of all points that are less than `δ` distance away from some point in `s`.
More concisely: For any seminormed additive commutative group E, subset s, and real number δ, the set {x : E | ∥x∥ ≤ δ ∨ x ∈ s} equals the set {x : E | ∥x - o ∥ ≤ δ}, where o is the origin of E.
|
IsCompact.add_closedBall_zero
theorem IsCompact.add_closedBall_zero :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
IsCompact s → 0 ≤ δ → s + Metric.closedBall 0 δ = Metric.cthickening δ s
This theorem states that for any given compact set 's' in a semi-normed additive commutative group 'E', and for any non-negative real number 'δ', the set obtained by adding 's' and the closed ball of radius 'δ' centered at 0 is equal to the closed δ-thickening of 's'. In other words, the sum of 's' and the closed ball of radius 'δ' centered at 0 expands 's' by a thickness of 'δ', without changing its essential structure.
More concisely: For any compact set 's' in a semi-normed additive commutative group 'E' and real number 'δ'≥0, the sum of 's' and the closed ball of radius 'δ' centered at 0 equals the closed δ-thickening of 's'.
|
mul_ball_one
theorem mul_ball_one :
∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E), s * Metric.ball 1 δ = Metric.thickening δ s
The theorem `mul_ball_one` states that for any subset `s` of a semi-normed commutative group `E` and any real number `δ`, the product of `s` and the set of all points within distance `δ` from the identity element is the same as the `δ`-thickening of `s`. In other words, the set of all elements obtained by multiplying an element of `s` with another element that is within a distance `δ` from the identity element in `E`, is the same as the set of all elements in `E` that are within a distance `δ` from some element in `s`.
More concisely: For any semi-normed commutative group E and subset s, the set of products of an element in s with another element within distance δ from the identity in E is equal to the δ-thickening of s.
|
ball_mul_one
theorem ball_mul_one :
∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E), Metric.ball 1 δ * s = Metric.thickening δ s
This theorem states that for any set `s` in a semi-normed commutative group `E`, and any real number `δ`, the set of all points within distance `δ` from `1` in the set `s` (denoted by `Metric.ball 1 δ * s`) is equal to the `δ`-thickening of the set `s` (denoted by `Metric.thickening δ s`). The `δ`-thickening of a set is the set of all points that are less than a distance `δ` away from any point in the set.
More concisely: For any semi-normed commutative group `E` and set `s` in it, and real number `δ`, the `Metric.ball 1 δ` around `1` in `s` equals the `Metric.thickening δ` of `s`.
|