Set.Finite.isClosed_convexHull
theorem Set.Finite.isClosed_convexHull :
∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] [inst_5 : T2Space E] {s : Set E},
s.Finite → IsClosed ((convexHull ℝ) s)
This theorem states that the convex hull of a finite set is closed. Here, we consider a set `s` of elements of some type `E`. The type `E` is endowed with several structures: it is an additive commutative group, a module over the real numbers `ℝ`, equipped with a topological structure that makes it a topological additive group, and the scalar multiplication is assumed to be continuous. Furthermore, `E` is a `T2` (or Hausdorff) space. Under these conditions, if the set `s` is finite, then the convex hull of `s` - which is defined as the smallest convex set containing `s` - is a closed set in the topological sense. In other words, it contains all its limit points.
More concisely: The convex hull of a finite set in a topological additive group endowed with a continuous scalar multiplication and a T2 topology is a closed set.
|
Convex.combo_closure_interior_subset_interior
theorem Convex.combo_closure_interior_subset_interior :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s → ∀ {a b : 𝕜}, 0 ≤ a → 0 < b → a + b = 1 → a • closure s + b • interior s ⊆ interior s
The theorem `Convex.combo_closure_interior_subset_interior` states that if `s` is a convex set in a topological vector space `E` over a linearly ordered field `𝕜`, then for any real numbers `a` and `b` such that `a` is nonnegative, `b` is positive, and `a + b` equals 1, the set resulting from taking the `a`-scaled closure of `s` and adding it to the `b`-scaled interior of `s` is a subset of the interior of `s`. This theorem is a stronger version of `Convex.combo_self_interior_subset_interior`. This property is important in understanding the topological properties of convex sets.
More concisely: If `s` is a convex set in a topological vector space over a linearly ordered field, then for any nonnegative real number `a` and positive real number `b` with `a + b = 1`, the `a`-scaled closure of `s` intersects the `b`-scaled interior of `s`, and their union is a subset of the interior of `s`.
|
isClosed_stdSimplex
theorem isClosed_stdSimplex : ∀ (ι : Type u_1) [inst : Fintype ι], IsClosed (stdSimplex ℝ ι)
The theorem `isClosed_stdSimplex` states that for any type `ι` with a finite number of elements, the standard simplex in the space of functions from `ι` to the real numbers is a closed set. The standard simplex here is defined as the set of all functions from `ι` to the real numbers that assign a non-negative real number to each element of `ι` and whose sum over all elements of `ι` is 1. A set being closed in this context means it contains all its limit points.
More concisely: The standard simplex in the space of functions from a finite type `ι` to the real numbers, defined as the set of functions with non-negative values summing to 1, is a closed set.
|
Convex.strictConvex
theorem Convex.strictConvex :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s → ((s \ interior s).Pairwise fun x y => (segment 𝕜 x y \ frontier s).Nonempty) → StrictConvex 𝕜 s
The theorem `Convex.strictConvex` states that for any Convex set `s` in a given Linear Ordered Field `𝕜` and Additive Commutative Group `E`, where `E` is also a Topological Space and a Topological Additive Group with a Continuous Constant Scalar Multiplication from `𝕜`, `s` is strictly convex if for any pair of distinct points `x` and `y` in the set difference of `s` and its interior, the open segment formed by `x` and `y` has a non-empty intersection with the interior of `s`, excluding the frontier of `s`. In simpler terms, a convex set is strictly convex if any line segment connecting two distinct points in the set, excluding the boundary, has a point in the set's interior.
More concisely: A convex set in a Linear Ordered Field with Continuous Scalar Multiplication is strictly convex if any open segment between distinct points in the set difference and its interior intersects the interior of the set, excluding its frontier.
|
Convex.subset_interior_image_homothety_of_one_lt
theorem Convex.subset_interior_image_homothety_of_one_lt :
∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] {s : Set E},
Convex ℝ s → ∀ {x : E}, x ∈ interior s → ∀ (t : ℝ), 1 < t → s ⊆ interior (⇑(AffineMap.homothety x t) '' s)
The theorem `Convex.subset_interior_image_homothety_of_one_lt` states that for a convex set in a real vector space with a given topological structure, if we perform a dilation (homothety) operation on the set about a point in its interior with a scale factor greater than 1, then the interior of the resulting set includes the closure of the original set. This theorem is currently applicable to convex sets and there is a plan to extend it to sets that are balanced or star-shaped about a given point.
More concisely: If A is a convex set in a real vector space with a given topological structure, and p is a point in the interior of A, then the interior of the set obtained by dilating A about p with a scale factor greater than 1 includes the closure of A.
|
Convex.combo_interior_closure_subset_interior
theorem Convex.combo_interior_closure_subset_interior :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s → ∀ {a b : 𝕜}, 0 < a → 0 ≤ b → a + b = 1 → a • interior s + b • closure s ⊆ interior s
The theorem `Convex.combo_interior_closure_subset_interior` states that given a convex set `s` in a topological space with an additive group structure, and a module over a linearly ordered field, if `a` and `b` are scalars such that `a` is positive, `b` is non-negative, and their sum equals 1, then the set formed by adding `a` times the interior of `s` and `b` times the closure of `s` is a subset of the interior of `s`. This extends a weaker version of the theorem, `Convex.combo_interior_self_subset_interior`, which holds for similar conditions.
More concisely: Given a convex set `s` in a topological space with an additive group structure and over a linearly ordered field, if `a` and `b` are scalars with `a` positive, `b` non-negative, and `a + b = 1`, then the intersection of `a * Int(s)` and `b * Cl(s)` is a subset of `Int(s)`.
|
Convex.add_smul_mem_interior'
theorem Convex.add_smul_mem_interior' :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s →
∀ {x y : E}, x ∈ closure s → x + y ∈ interior s → ∀ {t : 𝕜}, t ∈ Set.Ioc 0 1 → x + t • y ∈ interior s
This theorem states that for a convex set `s` in a given topological space, if a point `x` is in the closure of `s` and another point `x + y` is in the interior of `s`, then for any real number `t` in the interval `(0, 1]`, the point `x + t * y` is also in the interior of `s`. Here, the closure of a set is the smallest closed set containing that set, the interior of a set is its largest open subset, and `(0, 1]` refers to the interval that is open at `0` and closed at `1`.
More concisely: If a point `x` is in the closure of a convex set `s` and another point `x + y` is in the interior of `s`, then for any `t` in `(0, 1]`, the point `x + t * y` is in the interior of `s`.
|
isCompact_stdSimplex
theorem isCompact_stdSimplex : ∀ (ι : Type u_1) [inst : Fintype ι], IsCompact (stdSimplex ℝ ι)
The theorem `isCompact_stdSimplex` states that for any type `ι`, given that `ι` is finite (Fintype `ι`), the standard simplex in the space of functions from `ι` to real numbers (`ι → ℝ`) is compact. In other words, the set of all functions from `ι` to the real numbers, where each function produces non-negative real numbers and the sum of the function's values over all elements of `ι` is 1, forms a compact set in the topological space sense. Here, a set is called compact if for every nontrivial filter that contains the set, there exists an element in the set such that every set in the filter intersects every neighborhood of that element.
More concisely: Given a finite type `ι`, the set of functions from `ι` to real numbers that map each element to a non-negative number with sum 1 forms a compact subset in the topological space of real-valued functions on `ι`.
|
IsPreconnected.convex
theorem IsPreconnected.convex : ∀ {s : Set ℝ}, IsPreconnected s → Convex ℝ s
The theorem `IsPreconnected.convex` states that for any set `s` of real numbers, if `s` is preconnected, then `s` is also convex. In other words, if there is no non-trivial open partition of the set `s` (which is the definition of `s` being preconnected), then for any element `x` in `s`, the set `s` is star-convex at `x` (which means `s` is convex). This is essentially the reverse direction of the theorem `Real.convex_iff_isPreconnected`.
More concisely: If a set of real numbers is preconnected, then it is convex.
|
Convex.add_smul_mem_interior
theorem Convex.add_smul_mem_interior :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s → ∀ {x y : E}, x ∈ s → x + y ∈ interior s → ∀ {t : 𝕜}, t ∈ Set.Ioc 0 1 → x + t • y ∈ interior s
The theorem `Convex.add_smul_mem_interior` states that if we have a convex set `s` in a topological vector space over a linearly ordered field, then for any elements `x` and `y` of the space, if `x` is in `s` and `x + y` is in the interior of `s`, then `x + t * y` is also in the interior of `s` for any scalar `t` that lies in the interval (0, 1] (i.e., `t` is greater than 0 and less than or equal to 1). Here, the interior of a set is the largest open subset of `s` and the scalar multiplication `t * y` is denoted by `t • y` in the code.
More concisely: If `x` is in the interior of a convex set `s` in a topological vector space over a linearly ordered field, and `x + y` is in `s`, then for any `0 < t <= 1`, `x + t • y` is in the interior of `s`.
|
Convex.closure
theorem Convex.closure :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s → Convex 𝕜 (closure s)
This theorem states that in a topological vector space, if a set is convex, then its closure is also convex. Here, a topological vector space is denoted by `E` which is a commutative additive group (denoted by `AddCommGroup E`) with a topology (denoted by `TopologicalSpace E`), a scalar field denoted by `𝕜` which is a linearly ordered field, and a scalar multiplication operation (denoted by `Module 𝕜 E`). The closure operation is defined as the smallest closed set that contains the original set, and convexity is defined such that for any two points in the set, all points on the line segment that joins them are also in the set. The theorem asserts that if a set `s` in `E` is convex, then the closure of `s` is also convex.
More concisely: In a topological vector space, the closure of a convex set is convex.
|
Convex.isConnected
theorem Convex.isConnected :
∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] {s : Set E},
Convex ℝ s → s.Nonempty → IsConnected s
This theorem states that if a set in a vector space is nonempty and convex, then it is also connected. Here, a convex set is one in which every line segment connecting two points within the set is entirely contained in the set, and a connected set is one that cannot be partitioned into two nonempty open sets. The vector space is equipped with a topology that makes the addition operation continuous and also allows scalar multiplication to be continuous.
More concisely: If a nonempty, convex subset of a vector space, endowed with a topology making addition and scalar multiplication continuous, is also connected.
|
Convex.add_smul_sub_mem_interior
theorem Convex.add_smul_sub_mem_interior :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s → ∀ {x y : E}, x ∈ s → y ∈ interior s → ∀ {t : 𝕜}, t ∈ Set.Ioc 0 1 → x + t • (y - x) ∈ interior s
The theorem `Convex.add_smul_sub_mem_interior` states that for a convex set `s` in a linear ordered field `𝕜` and an additive commutative group `E` that is also a 𝕜-module with a topological structure, a topological additive group structure, and where scalar multiplication by a constant is continuous, if `x` is an element of `s` and `y` is in the interior of `s`, then for any `t` in the half-open interval (0, 1) (i.e., 0 < t ≤ 1), the point obtained by taking `x` and moving `t` of the way toward `y` (formally, `x + t • (y - x)`) is an element of the interior of `s`. This theorem essentially states that within a convex set, any point partway along the line segment from a point in the set to a point in the interior of the set is also in the interior of the set.
More concisely: Given a convex set in a linear ordered field with additional structure, if an element is in the set and another element is in its interior, then every point on the line segment between them is also in the interior of the set.
|
Convex.interior
theorem Convex.interior :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s → Convex 𝕜 (interior s)
This theorem states that in a topological vector space, if a set is convex, then its interior is also convex. In more detail, given a type 𝕜 which is a linearly ordered field, a type E with a structure of an additive commutative group, a 𝕜-module structure on E, a topology on E which turns it into a topological space, a topological additive group structure, and a continuity of scalar multiplication, then for any set s of elements of type E, if s is convex, then the interior of s (the largest open subset of s) is also convex.
More concisely: In a topological vector space over a linearly ordered field, the interior of a convex set is convex.
|
Convex.combo_interior_self_subset_interior
theorem Convex.combo_interior_self_subset_interior :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s → ∀ {a b : 𝕜}, 0 < a → 0 ≤ b → a + b = 1 → a • interior s + b • s ⊆ interior s
This theorem, 'Convex.combo_interior_self_subset_interior', states that for any convex set `s` in a topological vector space `E` over a linearly ordered field `𝕜`, if `a` and `b` are scalars such that `0 < a`, `0 ≤ b`, and `a + b = 1`, then the Minkowski sum of `a` times the interior of `s` and `b` times `s` is a subset of the interior of `s`. Essentially, it explains that a certain linear combination of the interior and the whole set, under specific conditions, lies within the interior of the set. This theorem is related to the subset property of convex sets in a topological vector space.
More concisely: For any convex set `s` in a topological vector space `E` over a linearly ordered field `𝕜`, the Minkowski sum of `a` times the interior of `s` and `b` times `s` lies in the interior of `s`, where `0 < a`, `0 ≤ b`, and `a + b = 1`.
|
stdSimplex_subset_closedBall
theorem stdSimplex_subset_closedBall : ∀ {ι : Type u_1} [inst : Fintype ι], stdSimplex ℝ ι ⊆ Metric.closedBall 0 1 := by
sorry
This theorem states that every vector in the standard simplex of a given type 𝕜 and index type ι has a maximum norm of at most 1. In other words, for any finite type ι, the standard simplex in the space of functions from ι to the reals is a subset of the closed ball in the metric space with radius 1 and centered at the origin. The standard simplex here refers to the set of all functions from ι to the reals such that all function values are non-negative and their sum is 1. The closed ball is defined as the set of all points whose distance from the origin is less than or equal to 1.
More concisely: The maximum norm of every function in the standard simplex of a finite type is at most 1. (The standard simplex being the set of functions from the type to the reals with non-negative values and sum equal to 1.)
|
TopologicalAddGroup.pathConnectedSpace
theorem TopologicalAddGroup.pathConnectedSpace :
∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : TopologicalAddGroup E] [inst : ContinuousSMul ℝ E], PathConnectedSpace E
This theorem states that every topological vector space over the real numbers (ℝ) is path connected. In more detail, for any type `E` that is an additive commutative group, a module over ℝ, a topological space, a topological additive group, and has a continuous scalar multiplication operation, the space `E` is path connected. Note that this theorem is not instantiated due to the potential creation of large type class subproblems.
More concisely: Every topological vector space over the real numbers is a path-connected topological group.
|
Convex.combo_self_interior_subset_interior
theorem Convex.combo_self_interior_subset_interior :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s → ∀ {a b : 𝕜}, 0 ≤ a → 0 < b → a + b = 1 → a • s + b • interior s ⊆ interior s
The theorem `Convex.combo_self_interior_subset_interior` states that for any convex set `s` in a topological vector space `E` over a linearly ordered field `𝕜`, and any non-negative real numbers `a` and `b` such that `a + b = 1` with `b > 0`, the set formed by the sum of the scalar multiplication of `a` with `s` and the scalar multiplication of `b` with the interior of `s` is a subset of the interior of `s`. In other words, if you scale and add the set `s` and its interior, the resulting set will still be within the interior of `s`. The theorem also notes that there is a stronger version of this statement, `Convex.combo_closure_interior_subset_interior`.
More concisely: For any convex set `s` in a topological vector space over a linearly ordered field, and any `a, b ∈ ℝ` with `a ≥ 0`, `b > 0`, and `a + b = 1`, the set `{as ∪ b Int(s)}` is a subset of `Int(s)`.
|
Convex.isPreconnected
theorem Convex.isPreconnected :
∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] {s : Set E}, Convex ℝ s → IsPreconnected s
The theorem `Convex.isPreconnected` states that for any real vector space `E` equipped with an addition-commutative group structure, a Module over the reals, a topological space structure, a topological add group structure, and a continuous action of scalar multiplication, if a set `s` in this space is convex, then the set `s` is also preconnected. In terms of mathematics, a convex set is one where for any two points in the set, the entire line segment between these two points is also in the set. Preconnectedness is a topological property; a set is preconnected if there is no non-trivial open partition of the set. So, the theorem is asserting a connection between these two seemingly different properties — convexity and preconnectedness.
More concisely: If a convex set in a real vector space is equipped with additional structures, then it is preconnected.
|
Convex.closure_subset_image_homothety_interior_of_one_lt
theorem Convex.closure_subset_image_homothety_interior_of_one_lt :
∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] {s : Set E},
Convex ℝ s →
∀ {x : E}, x ∈ interior s → ∀ (t : ℝ), 1 < t → closure s ⊆ ⇑(AffineMap.homothety x t) '' interior s
This theorem states that for a convex set `s` in a real vector space `E` equipped with additional structures of topology, topological addition, and continuous scalar multiplication, if we take a point `x` in the interior of `s` and perform a dilation (also known as homothety) about `x` with a scale factor `t > 1`, the resulting set contains the closure of `s`. In other words, enlarging the interior of the convex set about a point in its interior by a factor greater than 1 will always include the original set along with its limit points. The theorem also notes a potential for future work to generalize this property from convex sets to balanced or star-shaped sets about `x`.
More concisely: Given a convex set `s` in a real vector space `E` with topology, topological addition, and continuous scalar multiplication, if `x` is an interior point of `s` and `t > 1`, then the dilated set `{y : E | ∃ z ∈ s, y = x + t*(z - x)}` contains the closure of `s`.
|
Convex.add_smul_sub_mem_interior'
theorem Convex.add_smul_sub_mem_interior' :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s →
∀ {x y : E}, x ∈ closure s → y ∈ interior s → ∀ {t : 𝕜}, t ∈ Set.Ioc 0 1 → x + t • (y - x) ∈ interior s
This theorem states that if a set `s` of elements of some type `E` is convex, and `x` and `y` are elements of `E` such that `x` is in the closure of `s` and `y` is in the interior of `s`, then for any scalar `t` from the interval `(0, 1]`, the point obtained by traveling from `x` towards `y` a proportion `t` of the way (formally, `x + t • (y - x)`) lies in the interior of `s`. This applies under certain conditions on the type `E` and the scalar field `𝕜`, specifically that `E` is a topological space with a continuous scalar multiplication and `𝕜` is a linear ordered field.
More concisely: If `s` is a convex subset of a topological space `E` with continuous scalar multiplication over a linear ordered field `𝕜`, then for any `x` in the closure of `s` and `y` in the interior of `s`, the point `x + t * (y - x)` lies in the interior of `s` for all `t` in the open interval `(0, 1]`.
|
Convex.isPathConnected
theorem Convex.isPathConnected :
∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] {s : Set E},
Convex ℝ s → s.Nonempty → IsPathConnected s
The theorem `Convex.isPathConnected` states that for any type `E`, given that `E` has the structure of an additive commutative group, a module over the reals, a topological space, a topological additive group, and that scalar multiplication is continuous, if `s` is a set of `E` with the property that it is convex and nonempty, then `s` is also path connected. In other words, for a nonempty set `s` in a real vector space that is convex, there exists a point in `s` that can be joined to all other points in `s` through a path that remains within `s`.
More concisely: In a real vector space endowed with the structure of an additive commutative group, a topological space, and a topological additive group, where scalar multiplication is continuous, every nonempty convex set is path connected.
|
Set.Finite.isCompact_convexHull
theorem Set.Finite.isCompact_convexHull :
∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] {s : Set E},
s.Finite → IsCompact ((convexHull ℝ) s)
The theorem `Set.Finite.isCompact_convexHull` asserts that the convex hull of any finite set is compact. More specifically, if `E` is a type with an addition group structure, a module structure over the real numbers, and a topological space structure, and if `s` is a finite set of elements of type `E`, then the convex hull of `s` (which is the smallest convex set that contains `s`) is a compact set. In topological terms, a set is compact if, for every nontrivial filter on the set, there exists an element in the set such that every set in the filter meets every neighborhood of that element. In this context, a filter is essentially a consistent way of choosing "large" subsets of the set, and a neighborhood of an element is any open set that contains that element.
More concisely: The convex hull of any finite set in a topological vector space is a compact set.
|
Convex.closure_subset_interior_image_homothety_of_one_lt
theorem Convex.closure_subset_interior_image_homothety_of_one_lt :
∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] {s : Set E},
Convex ℝ s →
∀ {x : E}, x ∈ interior s → ∀ (t : ℝ), 1 < t → closure s ⊆ interior (⇑(AffineMap.homothety x t) '' s)
This theorem states that for a given convex set in a real vector space with a topology, if we choose a point from the interior of this set and dilate the set about this point using a scale factor greater than 1, then the interior of the resulting set will contain the closure of the original set.
In other words, when we expand a convex set uniformly in all directions from a point within it by a factor greater than one, the boundary and interior of the original set will be entirely contained within the interior of the resulting set. This theorem is yet to be generalized from convex sets to sets that are balanced or star-shaped around a point.
More concisely: For a convex set in a real vector space with a topology, dilating it from an interior point using a scale factor greater than 1 results in a larger set whose interior contains the closure of the original set.
|
bounded_stdSimplex
theorem bounded_stdSimplex : ∀ (ι : Type u_1) [inst : Fintype ι], Bornology.IsBounded (stdSimplex ℝ ι)
The theorem `bounded_stdSimplex` states that for any type `ι` that has a `Fintype` instance, the standard simplex in the space of functions from `ι` to real numbers (`ℝ`) is bounded. This is in relation to the ambient bornology on the set of such functions. In other words, the set of all functions from `ι` to `ℝ` that assign non-negative values to each element of `ι` such that the sum of all these values equals 1, is a bounded set.
More concisely: The standard simplex of functions from a type with a `Fintype` instance to real numbers, mapping each element to non-negative values summing up to 1, is a bounded set.
|
Convex.strictConvex'
theorem Convex.strictConvex' :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {s : Set E},
Convex 𝕜 s →
((s \ interior s).Pairwise fun x y => ∃ c, (AffineMap.lineMap x y) c ∈ interior s) → StrictConvex 𝕜 s
This theorem states that a convex set `s` is strictly convex if and only if for any two different points in the set `s` that are not in the interior of `s`, there exists a point on the line passing through these two points that lies in the interior of `s`. Here, `𝕜` is a linear ordered field that serves as the scalar field, `E` is an additive group that has a `𝕜`-module structure, and also has a topology where addition and scalar multiplication are continuous operations.
More concisely: A convex set in a linear ordered field with a continuous scalar multiplication and addition topology is strictly convex if and only if for any two distinct points not in its interior, there exists a point on the line passing through them that lies in the set's interior.
|