isConnected_setOf_sameRay
theorem isConnected_setOf_sameRay :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E),
IsConnected {y | SameRay ℝ x y}
The theorem states that for any vector `x` in a semi-normed additive commutative group `E` that also forms a normed space over the real numbers, the set of all vectors that are in the same ray as `x` is connected. Here, a set is connected if it is nonempty and if there is no non-trivial open partition. Two vectors are said to be in the same ray if one of them is a zero vector or if there exist positive multiples of both vectors such that the scaled vectors are equal.
More concisely: In a semi-normed additive commutative group `E` that is also a normed space over the real numbers, the set of all vectors in the same ray as a given vector `x` is a connected set.
|
convexOn_univ_norm
theorem convexOn_univ_norm :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E], ConvexOn ℝ Set.univ norm
The theorem `convexOn_univ_norm` states that for any real normed space E (which is also a seminormed add comm group), the norm function is convex on the entire space. In other words, for any two points x and y in the space, and any two non-negative real numbers a and b such that a + b = 1, the norm of the weighted sum a*x + b*y is less than or equal to the weighted sum of the norms a*norm(x) + b*norm(y). This property holds for the universal set, meaning it is true for all elements in the normed space E.
More concisely: For any normed space E, the norm function is convex, i.e., for all x, y in E and non-negative real numbers a, b with a + b = 1, we have a*||x|| + b*||y|| ≤ ||a*x + b*y||.
|
convexOn_norm
theorem convexOn_norm :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E},
Convex ℝ s → ConvexOn ℝ s norm
The theorem `convexOn_norm` states that for any type `E` endowed with a structure of a semi-normed additive commutative group and a real normed space, and any set `s` of type `E`, if the set `s` is convex, then the norm function on this real normed space is convex on `s`. In other words, for any two points in the set, a weighted average of their norms is at least as large as the norm of the corresponding weighted average of the points, where the weights are non-negative real numbers that sum to 1. This is a generalization of the triangle inequality in real normed spaces.
More concisely: Given a semi-normed additive commutative group `E` with a real normed space structure, if `s` is a convex subset of `E`, then the norm function is convex on `s`, i.e., for all `x, y in s` and `r in [0, 1]`, `||rx + (1-r)y|| <= r*||x|| + (1-r)*||y||`.
|
convexHull_diam
theorem convexHull_diam :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (s : Set E),
Metric.diam ((convexHull ℝ) s) = Metric.diam s
The theorem `convexHull_diam` states that for any set `s` of type `E` in a normed space over the real numbers, the diameter of the convex hull of `s` is equal to the diameter of `s` itself. In other words, the maximum distance between any two points in the convex hull of `s` is the same as the maximum distance between any two points in `s`. This implies that the process of forming the convex hull of a set does not extend the distance between the points in the set.
More concisely: The diameter of a convex hull of a set in a normed space equals the diameter of the set.
|
isBounded_convexHull
theorem isBounded_convexHull :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E},
Bornology.IsBounded ((convexHull ℝ) s) ↔ Bornology.IsBounded s
The theorem `isBounded_convexHull` states that for any set `s` of elements of type `E`, which is a semi-normed additive commutative group and a normed space over the reals, the convex hull of `s` is bounded if and only if `s` itself is bounded. In other words, the minimal convex set that includes `s` has bounds if and only if `s` has bounds, where boundedness is relative to the ambient bornology on the type `E`.
More concisely: The convex hull of a bounded semi-normed additive commutative group and normed space over the reals is bounded if and only if the group itself is bounded.
|
convexHull_exists_dist_ge
theorem convexHull_exists_dist_ge :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {x : E},
x ∈ (convexHull ℝ) s → ∀ (y : E), ∃ x' ∈ s, dist x y ≤ dist x' y
This theorem states that, for a given point `x` that lies within the convex hull of a set `s` and another point `y`, there exists a point `x'` in set `s` such that the distance between `x` and `y` is less than or equal to the distance between `x'` and `y`. The set `s` is in a normed space over the real numbers, which is also a semi-normed add commutative group.
More concisely: Given a point `x` in a convex hull of a set `s` in a normed space over the real numbers, and a point `y`, there exists a point `x'` in `s` such that the distance from `x` to `y` is less than or equal to the distance from `x'` to `y`.
|
convex_ball
theorem convex_ball :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (a : E) (r : ℝ),
Convex ℝ (Metric.ball a r)
The theorem `convex_ball` states that for any given type `E` that forms a seminormed additive commutative group and has a structure of a normed space over the real numbers, and for any element `a` of type `E` and any real number `r`, the metric ball around `a` with radius `r` is a convex set in the real number plane. In other words, if you take any two points inside this ball, then the whole line segment connecting these two points is also inside the ball.
More concisely: For any normed space `(E, ||·||)` over the real numbers and any `a ∈ E` and `r > 0`, the metric ball `{x ∈ E | ||x - a|| ≤ r}` is a convex set in `E`.
|
convexHull_exists_dist_ge2
theorem convexHull_exists_dist_ge2 :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s t : Set E} {x y : E},
x ∈ (convexHull ℝ) s → y ∈ (convexHull ℝ) t → ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
The theorem `convexHull_exists_dist_ge2` states that for any two points `x` and `y`, where `x` is in the convex hull of a set `s` and `y` is in the convex hull of a set `t`, there exist points `x'` in `s` and `y'` in `t` such that the distance between `x` and `y` is less than or equal to the distance between `x'` and `y'`. This is stated in the context of a seminormed add commutative group `E` over the real numbers, which is also a normed space.
More concisely: If sets `s` and `t` have points `x` in the convex hull of `s` and `y` in the convex hull of `t` in a normed space `E` over the real numbers, then there exist points `x' in s` and `y' in t` such that `norm x - y ≤ norm x' - y'`.
|
convexHull_ediam
theorem convexHull_ediam :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (s : Set E),
EMetric.diam ((convexHull ℝ) s) = EMetric.diam s
The theorem `convexHull_ediam` states that for any set `s` of elements of type `E` in a normed space over the real numbers, the Emetric diameter of the convex hull of `s` is equal to the Emetric diameter of `s` itself. In other words, the maximum distance (as defined by the Emetric or extended metric) between any two points in the convex hull of a set is precisely the same as the maximum distance between any two points in the original set.
More concisely: The metric diameter of a convex hull is equal to the metric diameter of the set from which it is formed.
|
isConnected_setOf_sameRay_and_ne_zero
theorem isConnected_setOf_sameRay_and_ne_zero :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x : E},
x ≠ 0 → IsConnected {y | SameRay ℝ x y ∧ y ≠ 0}
The theorem `isConnected_setOf_sameRay_and_ne_zero` states that for any given non-zero vector `x` in a seminormed add commutative group `E` that is also a normed space over the real numbers, the set of all non-zero vectors that are in the same ray as `x` is a connected set. Here, two vectors are considered to be in the same ray if one is a positive multiple of the other or if one of them is zero. A set is considered connected if it is nonempty and there is no non-trivial open partition.
More concisely: The set of non-zero vectors in a seminormed add commutative group that is also a normed space over the real numbers, which are in the same ray as a non-zero vector `x`, forms a connected subset.
|