Convex.toCone_isLeast
theorem Convex.toCone_isLeast :
β {π : Type u_1} {E : Type u_2} [inst : LinearOrderedField π] [inst_1 : AddCommGroup E] [inst_2 : Module π E]
{s : Set E} (hs : Convex π s), IsLeast {t | s β βt} (Convex.toCone s hs)
The theorem `Convex.toCone_isLeast` states that for any type 'π' which forms a linear ordered field, and any type 'E' which forms an additive commutative group and a module over 'π', if 's' is a convex set of elements of type 'E' and 'hs' is the proof of this convexity, then the convex cone formed by vectors proportional to those in 's' (denoted as `Convex.toCone s hs`) is the least convex cone that includes 's'. This least convex cone is a part of the set of all convex cones 't' such that 's' is a subset of 't'.
More concisely: For any linear ordered field 'π' and additive commutative group/module 'E' over 'π', the convex cone `Convex.toCone` of a convex set 's' in 'E' is the least convex cone containing 's'.
|
ConvexCone.Blunt.salient
theorem ConvexCone.Blunt.salient :
β {π : Type u_1} {E : Type u_2} [inst : OrderedSemiring π] [inst_1 : AddCommGroup E] [inst_2 : SMul π E]
{S : ConvexCone π E}, S.Blunt β S.Salient
This theorem states that for any ordered semiring π and additive commutative group E, any blunt convex cone S in the vector space of π and E is always salient. Here, a "blunt" convex cone is defined as one that does not contain the zero vector, and a "salient" convex cone is one where for any non-zero vector in the cone, its negative is not in the cone.
More concisely: Given any blunt convex cone in the vector space of an ordered semiring and an additive commutative group, the cone is salient.
|
ConvexCone.smul_mem
theorem ConvexCone.smul_mem :
β {π : Type u_1} {E : Type u_2} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E] [inst_2 : SMul π E]
(S : ConvexCone π E) {c : π} {x : E}, 0 < c β x β S β c β’ x β S
This theorem states that for any semi-ring π, an additive commutative monoid E and a scalar multiplication operation between π and E, if we have a convex cone S in the vector space spanned by π and E, then for any scalar c from π and any vector x from E, if c is positive and x belongs to the convex cone S, then the scalar multiple c β’ x also belongs to the convex cone S. This essentially captures one of the key properties of a convex cone - it is closed under positive scalar multiplication.
More concisely: For any semi-ring π, additive commutative monoid E, and scalar multiplication between π and E, if S is a convex cone in the vector space spanned by π and E, then for all positive scalars c in π and vectors x in E, c β’ x is also in S.
|
ConvexCone.salient_strictlyPositive
theorem ConvexCone.salient_strictlyPositive :
β (π : Type u_1) (E : Type u_2) [inst : OrderedSemiring π] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module π E]
[inst_3 : OrderedSMul π E], (ConvexCone.strictlyPositive π E).Salient
The theorem `ConvexCone.salient_strictlyPositive` states that for any ordered semiring `π` and any ordered additive commutative group `E` that is also a `π`-module with ordered scalar multiplication, the strictly positive cone of `E` (defined as the set of elements greater than zero) is always salient. In the context of convex cones, a cone is said to be salient if it does not contain any line through the origin; in other words, it does not contain any pair of distinct points `x` and `-x`.
More concisely: For any ordered semiring `π` and ordered additive commutative group `E` that is a `π`-module with ordered scalar multiplication, the strictly positive cone of `E` is a salient convex cone.
|
ConvexCone.pointed_positive
theorem ConvexCone.pointed_positive :
β (π : Type u_1) (E : Type u_2) [inst : OrderedSemiring π] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module π E]
[inst_3 : OrderedSMul π E], (ConvexCone.positive π E).Pointed
The theorem `ConvexCone.pointed_positive` states that the positive cone of an ordered module is always pointed. In other words, for any ordered semiring π and ordered additive commutative group E with π acting as a module on E and the scalar multiplication being ordered, the convex cone formed by the set of nonnegative elements in E always contains the zero vector.
More concisely: The positive cone of an ordered module is a nonempty subset that contains the zero vector.
|
ConvexCone.add_mem
theorem ConvexCone.add_mem :
β {π : Type u_1} {E : Type u_2} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E] [inst_2 : SMul π E]
(S : ConvexCone π E) β¦x : Eβ¦, x β S β β β¦y : Eβ¦, y β S β x + y β S
This theorem states that for any ordered semiring `π` and additively commutative monoid `E`, if `S` is a convex cone in `E` over `π`, then for any elements `x` and `y` in `S`, their sum `x + y` is also in `S`. In other words, the convex cone `S` is closed under addition.
More concisely: If `S` is a convex cone over an ordered semiring `π` in an additively commutative monoid `E`, then `x`, `y` in `S` implies `x + y` is in `S`.
|
ConvexCone.Flat.pointed
theorem ConvexCone.Flat.pointed :
β {π : Type u_1} {E : Type u_2} [inst : OrderedSemiring π] [inst_1 : AddCommGroup E] [inst_2 : SMul π E]
{S : ConvexCone π E}, S.Flat β S.Pointed
This theorem asserts that for any convex cone `S` in a vector space `E` over an ordered semiring `π`, if `S` is flat, then `S` is also pointed, meaning it contains the zero vector. In other words, flatness of a convex cone implies that the cone contains the origin.
More concisely: If `S` is a convex cone in a vector space over an ordered semiring that is flat, then `S` contains the zero vector.
|
ConvexCone.blunt_strictlyPositive
theorem ConvexCone.blunt_strictlyPositive :
β (π : Type u_1) (E : Type u_2) [inst : OrderedSemiring π] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module π E]
[inst_3 : OrderedSMul π E], (ConvexCone.strictlyPositive π E).Blunt
This theorem states that for any ordered semiring `π` and any ordered additively commutative group `E` that is also a module over `π` with an ordered scalar multiplication, the strictly positive cone of the ordered module `E` is always blunt. The strictly positive cone is defined to be the set of all elements greater than 0 in this module. In this context, a convex cone being blunt means that it doesn't contain the element -1.
More concisely: For any ordered semiring `π` and ordered additively commutative group `E` that is a `π`-module with ordered scalar multiplication, the strictly positive cone of `E` is a blunt convex cone.
|
ConvexCone.mem_sInf
theorem ConvexCone.mem_sInf :
β {π : Type u_1} {E : Type u_2} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E] [inst_2 : SMul π E] {x : E}
{S : Set (ConvexCone π E)}, x β sInf S β β s β S, x β s
This theorem, `ConvexCone.mem_sInf`, states that for any types `π` and `E`, where `π` is an ordered semiring and `E` is an additive commutative monoid that also supports scalar multiplication by elements of `π`, a given element `x` of type `E` is in the infimum (greatest lower bound) of a set `S` of convex cones of `π` and `E` if and only if `x` is in every convex cone that is a member of `S`. A convex cone here refers to a subset of a vector space over a given field that is closed under linear combinations with positive coefficients.
More concisely: For any ordered semiring `π` and additive commutative monoid `E` with scalar multiplication, an element `x` of `E` lies in the infimum of a set `S` of convex cones of `π` and `E` if and only if it belongs to every convex cone in `S`.
|
ConvexCone.to_orderedSMul
theorem ConvexCone.to_orderedSMul :
β {π : Type u_1} {E : Type u_2} [inst : LinearOrderedField π] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module π E]
(S : ConvexCone π E), (β (x y : E), x β€ y β y - x β S) β OrderedSMul π E
This theorem, `ConvexCone.to_orderedSMul`, takes a convex cone `S` in the context of an ordered field `π`, an ordered additive commutative group `E`, and a module structure over `E` with scalar `π`. The theorem asserts that given a proof that the order relation is the one defined by the cone (in other words, for all `x` and `y` in `E`, `x` is less than or equal to `y` if and only if `y - x` is an element of `S`), the scalar multiplication operation `π Γ E β E` is compatible with the order, i.e., it creates an instance of `OrderedSMul π E`. This instance indicates that scalar multiplication respects the order relation on the scalars and the vectors, a necessary condition for a vector space with an ordered field as scalars.
More concisely: Given a convex cone `S` in an ordered field `π` with respect to an ordered additive commutative group `E` and a module structure over `E` with scalar `π`, if the order relation on `E` is defined by the cone, then scalar multiplication is order-preserving.
|
ConvexCone.salient_positive
theorem ConvexCone.salient_positive :
β (π : Type u_1) (E : Type u_2) [inst : OrderedSemiring π] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module π E]
[inst_3 : OrderedSMul π E], (ConvexCone.positive π E).Salient
The theorem `ConvexCone.salient_positive` states that for any given ordered semiring `π` and ordered additive commutative group `E` that also has a module structure and an ordered scalar multiplication, the positive cone of the ordered module is always salient. Here, a positive cone is defined as the convex cone formed by the set of nonnegative elements in the ordered module, and a cone is salient if, whenever it contains a vector, it doesn't contain the negative of that vector.
More concisely: In any ordered semiring with an ordered additive commutative group and module structure having ordered scalar multiplication, the positive cone is a salient cone.
|
ConvexCone.ext
theorem ConvexCone.ext :
β {π : Type u_1} {E : Type u_2} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E] [inst_2 : SMul π E]
{S T : ConvexCone π E}, (β (x : E), x β S β x β T) β S = T
The theorem `ConvexCone.ext` states that for any two convex cones `S` and `T` in a vector space `E` over an ordered semiring `π`, if every element `x` in `E` belongs to `S` if and only if it belongs to `T`, then `S` and `T` must be equal. In other words, two convex cones are equal if they contain exactly the same elements.
More concisely: If two convex cones in a vector space over an ordered semiring contain exactly the same elements, then they are equal.
|