exists_dist_eq
theorem exists_dist_eq :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x z : E) {a b : ℝ},
0 ≤ a → 0 ≤ b → a + b = 1 → ∃ y, dist x y = b * dist x z ∧ dist y z = a * dist x z
This theorem states that for any types `E` that form a seminormed additive commutative group and a normed space over the real numbers, given any two elements `x` and `z` of this type and any two non-negative real numbers `a` and `b` such that `a + b = 1`, there exists an element `y` in `E` such that the distance between `x` and `y` is equal to `b` times the distance between `x` and `z`, and the distance between `y` and `z` is equal to `a` times the distance between `x` and `z`.
More concisely: Given a seminormed additive commutative group `E` over the real numbers, for any `x`, `z` in `E` and `a`, `b` in `ℝ+` with `a + b = 1`, there exists `y` in `E` such that `||x - y|| = b * ||x - z||` and `||y - z|| = a * ||x - z||`.
|
affinity_unitClosedBall
theorem affinity_unitClosedBall :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
0 ≤ r → ∀ (x : E), x +ᵥ r • Metric.closedBall 0 1 = Metric.closedBall x r
This theorem states that for any real number `r` greater than or equal to zero, and for any element `x` of a normed additive commutative group `E` that's also a real normed space, the closed ball of radius `r` centered at `x` is equal to the image of the unit closed ball centered at 0 under the function that maps `y` to `x` plus `r` times `y`. In other words, the closed ball of any non-negative radius around any point in a normed space can be constructed by scaling and translating the unit ball.
More concisely: For any non-negative real number `r` and any point `x` in a normed additive commutative group `E` that's also a real normed space, the closed ball `{y | ||y-x|| ≤ r}` is equal to the image `{x + r*y | y ∈ B(0,1)}` under the function that maps `y` to `x + r*y`, where `B(0,1)` is the unit closed ball centered at the origin.
|
NormedSpace.sphere_nonempty
theorem NormedSpace.sphere_nonempty :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : Nontrivial E] {x : E} {r : ℝ},
(Metric.sphere x r).Nonempty ↔ 0 ≤ r
In a nontrivial real normed space, the theorem asserts that a sphere is nonempty if and only if its radius is nonnegative. More precisely, for any real normed additive commutative group `E` that is also a nontrivial real normed space, and for any point `x` in `E` and a real number `r`, the set of points `y` such that the distance from `y` to `x` equals `r` (the sphere centered at `x` with radius `r`) is nonempty if and only if `r` is greater than or equal to 0.
More concisely: In a nontrivial real normed space, a sphere centered at a point with non-negative radius is nonempty.
|
eventually_singleton_add_smul_subset
theorem eventually_singleton_add_smul_subset :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E},
Bornology.IsBounded s → ∀ {u : Set E}, u ∈ nhds x → ∀ᶠ (r : 𝕜) in nhds 0, {x} + r • s ⊆ u
The theorem `eventually_singleton_add_smul_subset` states that for a given field `𝕜` and a seminormed additive commutative group `E` with a normed space structure over `𝕜`, if `s` is a bounded set in `E` (as defined by the `Bornology.IsBounded` predicate), then for any set `u` that is a neighborhood of a point `x` in `E` (i.e., `u` belongs to the neighborhood filter at `x`), there exists a small enough scalar `r` in `𝕜` such that the scaled set `r • s` added to the singleton set containing `x` is contained within `u`. This containment holds eventually as `r` gets arbitrarily close to 0.
More concisely: For any bounded set `s` in a normed space `E` over a field `𝕜` and for any neighborhood `u` of a point `x` in `E`, there exists a scalar `r` close enough to 0 such that `r • s + {x} ⊆ u`.
|
smul_closedUnitBall_of_nonneg
theorem smul_closedUnitBall_of_nonneg :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
0 ≤ r → r • Metric.closedBall 0 1 = Metric.closedBall 0 r
In the context of a real normed space, the theorem `smul_closedUnitBall_of_nonneg` states that, for any nonnegative real number `r`, multiplying the unit closed ball by `r` results in a closed ball with a radius of `r` and centered at the origin. Here, a unit closed ball refers to the set of all points whose distance from the origin is less than or equal to 1. The operation of multiplying the unit closed ball by `r` scales the distances of the points in the ball from the origin by a factor of `r`. Thus, the resulting set of points forms a closed ball of radius `r` centered at the origin.
More concisely: In a real normed space, the set of points with distance from the origin less than or equal to 1 scaled by a nonnegative real number `r` forms a closed ball with radius `r` centered at the origin.
|
affinity_unitBall
theorem affinity_unitBall :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
0 < r → ∀ (x : E), x +ᵥ r • Metric.ball 0 1 = Metric.ball x r
This theorem states that for any given normed additive commutative group `E` and any real number `r` greater than 0 and any element `x` of `E`, any ball in the metric space with center `x` and radius `r` can be obtained as the image of the unit ball under the map `y ↦ x + r • y`. In simpler terms, it means that we can get any ball in the space by scaling the unit ball by a factor of `r` and then translating it by `x`. This is essentially the affinity transformation applied to the unit ball.
More concisely: For any normed additive commutative group `E`, real number `r` > 0, and element `x` in `E`, the ball with center `x` and radius `r` is equal to the image of the unit ball under the translation and dilation `y ↦ x + r • y`.
|
Bornology.IsBounded.smul₀
theorem Bornology.IsBounded.smul₀ :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {s : Set E}, Bornology.IsBounded s → ∀ (c : 𝕜), Bornology.IsBounded (c • s)
The theorem `Bornology.IsBounded.smul₀` states that for any type `𝕜`, which is a normed field, and any type `E`, which is a seminormed additive commutative group and a normed space over `𝕜`, if a set `s` of type `E` is bounded (in the sense defined by `Bornology.IsBounded`), then the image of the set `s` under scalar multiplication by any constant `c` of type `𝕜` is also bounded. This theorem is related to another lemma `Bornology.IsBounded.smul`, which deals with the similar situation for isometric actions.
More concisely: For any normed field `𝕜` and seminormed additive commutative group and normed space `E` over `𝕜`, if `s` is a bounded set in `E` then the image of `s` under scalar multiplication by any constant in `𝕜` is also bounded.
|
smul_ball
theorem smul_ball :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {c : 𝕜},
c ≠ 0 → ∀ (x : E) (r : ℝ), c • Metric.ball x r = Metric.ball (c • x) (‖c‖ * r)
The theorem `smul_ball` states that for any non-zero scalar `c`, any point `x`, and any real number `r`, the scaled version of a metric ball centered at `x` with radius `r` is equal to the metric ball centered at the scaled point `c • x` with radius `‖c‖ * r`. Here `𝕜` represents the normed field, `E` represents the semi-normed additive commutative group, and `Metric.ball x r` denotes the set of all points `y` such that the distance between `y` and `x` is less than `r`. This theorem is a property in the context of normed spaces.
More concisely: For any non-zero scalar `c` in a normed field `𝕜`, any point `x` in a semi-normed additive commutative group `E`, and any real number `r`, the metric ball `Metric.ball x r` is equal to `Metric.ball (c • x) (‖c��|| * r)`.
|
smul_sphere'
theorem smul_sphere' :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {c : 𝕜},
c ≠ 0 → ∀ (x : E) (r : ℝ), c • Metric.sphere x r = Metric.sphere (c • x) (‖c‖ * r)
The theorem `smul_sphere'` states that for any non-zero scalar `c` of a normed field `𝕜`, and any point `x` in a seminormed add commutative group `E` that also forms a normed space over `𝕜`, and any real number `r`, the scalar multiplication of `c` with the metric sphere centered at `x` with radius `r` equals the metric sphere centered at `c • x` with radius `‖c‖ * r`. In other words, scaling a sphere by a factor `c` not only scales the points in the sphere, but also moves its center and changes its radius proportionally to the absolute value of `c`.
More concisely: For any non-zero scalar `c` in a normed field and any point `x` in a seminormed add commutative group that is also a normed space over that field, the metric sphere centered at `x` with radius `r` is equal to the scalar multiplication of the sphere centered at `0` with radius `r * ‖c‖` by `c`, i.e., `{y : E | ∥y - x∥ ≤ r} = {y : E | ∥y - (c * x)∥ = r * ‖c‖}`.
|
smul_unitBall_of_pos
theorem smul_unitBall_of_pos :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
0 < r → r • Metric.ball 0 1 = Metric.ball 0 r
This theorem states that in a real normed space, if we take the unit ball (which is defined as the set of all points `y` such that their distance from the origin `0` is less than `1`) and scale it by a positive constant `r`, we end up with the ball of radius `r`. In other words, scalar multiplication of the unit ball by a positive constant `r` transforms it into a ball with radius `r`. This holds true for any type `E` which is a seminormed add commutative group and has a real normed space structure.
More concisely: In a real normed space, scaling the unit ball by a positive constant results in a ball of that radius.
|