convexHull_empty
theorem convexHull_empty :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E],
(convexHull 𝕜) ∅ = ∅
The theorem `convexHull_empty` states that for any ordered semiring `𝕜` and any type `E` which is an additive commutative monoid and also a module over `𝕜`, the convex hull of the empty set is the empty set. In other words, if we try to form the smallest convex set that includes no elements (i.e., the empty set), we end up with the empty set itself.
More concisely: The convex hull of the empty set is the empty set for an ordered semiring `𝕜`, an additive commutative monoid `E`, and a `𝕜`-module `E`.
|
convexHull_min
theorem convexHull_min :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
{s t : Set E}, s ⊆ t → Convex 𝕜 t → (convexHull 𝕜) s ⊆ t
The theorem `convexHull_min` states that for any ordered semiring `𝕜` and any additively commutative monoid `E` that is a `𝕜`-module, and for any two sets `s` and `t` of type `E`, if `s` is a subset of `t` and `t` is a convex set, then the convex hull of `s` is also a subset of `t`. In other words, the minimal convex set that includes `s` is contained within any larger convex set `t` that also contains `s`.
More concisely: For any ordered semiring 𝕜 and additively commutative monoid E that is a 𝕜-module, if s is a subset of the convex set t in E, then the convex hull of s is included in t.
|
convex_convexHull
theorem convex_convexHull :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
(s : Set E), Convex 𝕜 ((convexHull 𝕜) s)
The theorem `convex_convexHull` states that for any type `𝕜` with an ordered semiring structure, any type `E` with a structure of an additive commutative monoid and a module over `𝕜`, and any set `s` of type `E`, the convex hull of `s` is a convex set. In other words, the minimal convex set that includes `s` is itself convex. This is a fundamental property in the theory of convex sets in linear spaces.
More concisely: For any ordered semiring `𝕜`, additive commutative monoid and `𝝈`-module `E`, and set `s` of `E`, the convex hull of `s` is a convex set.
|
Convex.convexHull_eq
theorem Convex.convexHull_eq :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
{s : Set E}, Convex 𝕜 s → (convexHull 𝕜) s = s
This theorem states that for any ordered semiring `𝕜` and any set `s` in an additive commutative monoid `E` over which `𝕜` is a module, if `s` is a convex set, then the convex hull of `s` is equal to `s` itself. In other words, a convex set contains all the points in its convex hull.
More concisely: For any ordered semiring `𝕜` and additive commutative monoid `E` over which `𝕜` is a module, if `s` is a convex subset of `E`, then `s` is equal to its convex hull.
|
subset_convexHull
theorem subset_convexHull :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
(s : Set E), s ⊆ (convexHull 𝕜) s
This theorem states that for any given set `s` of type `E` within a module over an ordered semiring `𝕜`, the set `s` is a subset of its convex hull. In other words, all elements of `s` are also elements of the convex hull of `s`. In mathematical terms, if `𝕜` is an ordered semiring, `E` is an additive commutative monoid that forms a module over `𝕜`, and `s` is a set of elements from `E`, then `s ⊆ convexHull 𝕜 s`.
More concisely: For any set `s` of elements from an additive commutative monoid `E` within a module over an ordered semiring `𝕜`, `s` is a subset of its convex hull.
|
convexHull_mono
theorem convexHull_mono :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
{s t : Set E}, s ⊆ t → (convexHull 𝕜) s ⊆ (convexHull 𝕜) t
The theorem `convexHull_mono` states that for any ordered semiring `𝕜` and any type `E` which forms a module over `𝕜`, if we have two sets `s` and `t` of type `E` such that `s` is a subset of `t`, then the convex hull of `s` is also a subset of the convex hull of `t`. In other words, if a set `s` is contained within a larger set `t`, then the smallest convex set that contains `s` is also contained within the smallest convex set that contains `t`.
More concisely: For any ordered semiring 𝕜 and module E over it, if s is a subset of t in E, then the convex hull of s is contained in the convex hull of t.
|
convexHull_pair
theorem convexHull_pair :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
(x y : E), (convexHull 𝕜) {x, y} = segment 𝕜 x y
The `convexHull_pair` theorem states that for any ordered semiring `𝕜`, and any type `E` that is both an additive commutative monoid and a `𝕜`-module, and for any two elements `x` and `y` of `E`, the convex hull of the set containing just `x` and `y` is exactly the segment between `x` and `y`. In other words, the smallest convex set that contains both `x` and `y` is the set of all points that can be obtained by taking a convex combination of `x` and `y`.
More concisely: Given an ordered semiring 𝕜, an additive commutative monoid and 𝕜-module E, the convex hull of {x, y} ⊆ E equals the line segment between x and y.
|
convexHull_singleton
theorem convexHull_singleton :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] (x : E),
(convexHull 𝕜) {x} = {x}
The theorem `convexHull_singleton` states that for any given type `𝕜`, which is an ordered semiring, and any type `E`, which is an additive commutative monoid and a module over `𝕜`, the convex hull of a singleton set `{x}` in `E` is the set itself, `{x}`. In more intuitive terms, this means that if we have a set consisting of only one element (singleton set), the smallest convex set that contains this element is the set containing the element itself.
More concisely: For any ordered semiring `𝕜` and additive commutative monoid `E` being a `𝕜`-module, the convex hull of a singleton set in `E` equals the set itself.
|
Set.Nonempty.convexHull
theorem Set.Nonempty.convexHull :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
{s : Set E}, s.Nonempty → ((convexHull 𝕜) s).Nonempty
This theorem states that for any non-empty set `s` of type `E` in a module over a ordered semiring `𝕜`, the convex hull of `s` is also non-empty. This essentially means that if we have a non-empty set of points in a vector space, the smallest convex set containing all these points, i.e., their convex hull, is also non-empty.
More concisely: For any non-empty subset `s` of an additive monoid `E` in a module over an ordered semiring, the convex hull of `s` is a non-empty set.
|