StarConvex.add_smul_mem
theorem StarConvex.add_smul_mem :
โ {๐ : Type u_1} {E : Type u_2} [inst : OrderedRing ๐] [inst_1 : AddCommGroup E] [inst_2 : Module ๐ E] {x y : E}
{s : Set E}, StarConvex ๐ x s โ x + y โ s โ โ {t : ๐}, 0 โค t โ t โค 1 โ x + t โข y โ s
This theorem, `StarConvex.add_smul_mem`, states that given a star-convex set `s` in an ordered ring `๐` and a module `E` (a structure that behaves like a vector space), if a point `x` is in `s` and the set is star-convex at `x`, then for any point `y` in the same set and a non-negative scalar `t` less than or equal to `1`, the point obtained by adding `x` and the scalar multiple of `y` (`x + t โข y`) is also in the set `s`. In other words, in a star-convex set, any point on the line segment between `x` and `y` (where `x` is a point in the set and `y` is any other point in the set) is also in the set.
More concisely: Given a star-convex set `s` in an ordered ring `๐` and an module `E`, if `x` is in `s`, `x` is star-convex at `x`, and `y` is also in `s`, then `x + t โข y` is in `s` for all `t โ ๐` with `0 โค t โค 1`.
|
Set.OrdConnected.starConvex
theorem Set.OrdConnected.starConvex :
โ {๐ : Type u_1} {E : Type u_2} [inst : OrderedSemiring ๐] [inst_1 : OrderedAddCommMonoid E] [inst_2 : Module ๐ E]
[inst_3 : OrderedSMul ๐ E] {x : E} {s : Set E},
s.OrdConnected โ x โ s โ (โ y โ s, x โค y โจ y โค x) โ StarConvex ๐ x s
The theorem `Set.OrdConnected.starConvex` states that for any ordered semiring `๐`, any ordered additive commutative monoid `E` which is also a module over `๐`, any set `s` of elements of `E`, and any element `x` in `E`, if `s` is an order-connected set and all elements of `s` are comparable with `x` (i.e., for every element `y` in `s`, either `x` is less than or equal to `y` or `y` is less than or equal to `x`), and `x` is an element of `s`, then `s` is star-convex at `x`. In more intuitive terms, this means that if we have a set where the elements can be arranged in a certain order, and we can compare all elements in the set with a specific element `x` in the set, then the set is star-convex with respect to `x`. Star-convexity here means that for any point `y` in the set, the entire line segment connecting `x` and `y` is contained within the set.
More concisely: For any ordered semiring `๐`, ordered additive commutative monoid `E` over `๐`, and an order-connected set `s` of elements in `E` all comparable with an element `x` in `s`, if `x` is in `s`, then `s` is star-convex at `x`, i.e., the line segment connecting any `y` in `s` to `x` is contained in `s`.
|
StarConvex.affine_preimage
theorem StarConvex.affine_preimage :
โ {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [inst : OrderedRing ๐] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module ๐ E] [inst_4 : Module ๐ F] {x : E} (f : E โแต[๐] F) {s : Set F},
StarConvex ๐ (f x) s โ StarConvex ๐ x (โf โปยน' s)
This theorem states that if a set in affine space is star-convex, then its preimage under an affine map also retains this property. More specifically, given a type ๐ with an ordered ring structure, two types E and F with additive commutative group structures and ๐-module structures, an affine map from E to F, and a subset of F, if the subset is star-convex at the image of a point under the affine map, then the preimage of this subset under the affine map is star-convex at the original point. In other words, if a set is star-convex at a point, then the set of points mapped to it by an affine transformation is star-convex at the corresponding point under the inverse of this transformation.
More concisely: If a subset of an affine space is star-convex at its image under an affine map, then the preimage of that subset is star-convex at the original point.
|
StarConvex.ordConnected
theorem StarConvex.ordConnected :
โ {๐ : Type u_1} [inst : LinearOrderedField ๐] {x : ๐} {s : Set ๐}, x โ s โ StarConvex ๐ x s โ s.OrdConnected := by
sorry
This theorem, named `StarConvex.ordConnected`, states that for any linearly ordered field `๐`, and any set `s` of elements from `๐`, if an element `x` belongs to `s` and `s` is star-convex at `x`, then `s` is order-connected.
In mathematical terms, this means that whenever `s` is a star-convex set in the context of a linearly ordered field, and `x` is an element of `s`, then every interval formed by two points in `s` is entirely contained in `s`.
More concisely: In a linearly ordered field, if a star-convex set contains an element and is star-convex at that element, then the set is order-connected.
|
starConvex_compl_Ici
theorem starConvex_compl_Ici :
โ {๐ : Type u_1} {E : Type u_2} [inst : OrderedRing ๐] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module ๐ E]
[inst_3 : OrderedSMul ๐ E] {x y : E}, x < y โ StarConvex ๐ x (Set.Ici y)แถ
The theorem `starConvex_compl_Ici` states that for any ordered ring `๐`, any ordered add commutative group `E` that is also a `๐`-module with a compatible ordering, and any two elements `x` and `y` of `E` such that `x < y`, the set of all elements greater than or equal to `y` (`Set.Ici y`) is not star-convex at `x`. In other words, not every line segment from `x` to a point in the set of elements greater than or equal to `y` is entirely contained in that set.
More concisely: For any ordered ring `๐`, ordered add commutative group `E` that is an `๐`-module with a compatible ordering, and elements `x < y` in `E`, the set of elements greater than or equal to `y` does not contain every line segment from `x` to any of its elements.
|
StarConvex.affine_image
theorem StarConvex.affine_image :
โ {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [inst : OrderedRing ๐] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module ๐ E] [inst_4 : Module ๐ F] {x : E} (f : E โแต[๐] F) {s : Set E},
StarConvex ๐ x s โ StarConvex ๐ (f x) (โf '' s)
The theorem `StarConvex.affine_image` states that for any ordered ring `๐`, additive commutative groups `E` and `F`, `๐`-modules `E` and `F`, a point `x` in `E`, and an affine map `f` from `E` to `F`, if a set `s` in `E` is star-convex at `x` then its image under the affine map `f`, denoted by `(โf '' s)`, is star-convex at `f(x)`. In other words, the image of a star-convex set under an affine map remains star-convex.
Here, a set `s` is said to be star-convex at `x` if for every point `y` in `s`, any point on the line segment from `x` to `y` lies in `s`. The line segment from `x` to `y` is parameterized by `a โข x + b โข y` where `a` and `b` are non-negative numbers that add up to 1.
More concisely: The image of a star-convex set under an affine map is star-convex.
|
StarConvex.is_linear_image
theorem StarConvex.is_linear_image :
โ {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [inst : OrderedSemiring ๐] [inst_1 : AddCommMonoid E]
[inst_2 : AddCommMonoid F] [inst_3 : Module ๐ E] [inst_4 : Module ๐ F] {x : E} {s : Set E},
StarConvex ๐ x s โ โ {f : E โ F}, IsLinearMap ๐ f โ StarConvex ๐ (f x) (f '' s)
The theorem `StarConvex.is_linear_image` states that for any ordered semiring `๐`, types `E` and `F`, additive commutative monoids over `E` and `F`, modules over `๐` for `E` and `F`, a fixed point `x` in `E` and a set `s` in `E`, if the set `s` is star-convex at `x`, then for any linear map `f` from `E` to `F`, the image of the set `s` under `f` is star-convex at the image of `x` under `f`. In simpler terms, the image of a star-convex set under a linear map is also star-convex. The star-convexity is preserved under a linear transformation.
More concisely: For any ordered semiring ๐, additive commutative monoids E and F, modules over ๐ for E and F, and linear map f from E to F, if a set s in E is star-convex at x in E, then the image of s under f is star-convex at the image of x under f.
|
starConvex_compl_Iic
theorem starConvex_compl_Iic :
โ {๐ : Type u_1} {E : Type u_2} [inst : OrderedRing ๐] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module ๐ E]
[inst_3 : OrderedSMul ๐ E] {x y : E}, x < y โ StarConvex ๐ y (Set.Iic x)แถ
The theorem `starConvex_compl_Iic` states that for all types `๐` and `E`, where `๐` is an ordered ring and `E` is an ordered add commutative group with a `๐`-module structure and ordered scalar multiplication, given any two elements `x` and `y` of `E` such that `x < y`, the complement of the left-infinite right-closed interval at `x` (denoted as `(Set.Iic x)แถ`) is star-convex at `y`.
In other words, if `x < y`, then for any point `z` in the complement of the interval that includes all elements less than or equal to `x`, any line segment that connects `y` and `z` is entirely contained in the complement of this interval.
More concisely: For any ordered add commutative group `E` with a `๐`-module structure and ordered scalar multiplication over an ordered ring `๐`, if `x < y` in `E`, then the complement of the left-infinite right-closed interval at `x` is star-convex at `y`, that is, any line segment connecting `y` and any point in the complement of the interval lies entirely within the complement.
|
StarConvex.preimage_add_left
theorem StarConvex.preimage_add_left :
โ {๐ : Type u_1} {E : Type u_2} [inst : OrderedSemiring ๐] [inst_1 : AddCommMonoid E] [inst_2 : Module ๐ E]
{x z : E} {s : Set E}, StarConvex ๐ (x + z) s โ StarConvex ๐ x ((fun x => x + z) โปยน' s)
The theorem `StarConvex.preimage_add_left` states that for any ordered semiring `๐` and an additive commutative monoid `E` that is also a `๐`-module, if a set `s` of type `E` is star-convex at a point which is the sum of `x` and `z` of type `E`, then the translation of set `s` by `z` (i.e., the set of all elements `x'` such that `x'+z` belongs to `s`) is also star-convex at `x`. In other words, star-convexity is preserved under translation. This theorem allows us to shift the center of star-convexity from `x + z` to `x` by translating the set.
More concisely: If a star-convex set in an additive commutative `๐`-module `E` is centered at the sum of `x` and `z`, then translating the set by `-z` results in a star-convex set centered at `x`.
|
starConvex_iff_div
theorem starConvex_iff_div :
โ {๐ : Type u_1} {E : Type u_2} [inst : LinearOrderedField ๐] [inst_1 : AddCommGroup E] [inst_2 : Module ๐ E]
{x : E} {s : Set E},
StarConvex ๐ x s โ
โ โฆy : Eโฆ, y โ s โ โ โฆa b : ๐โฆ, 0 โค a โ 0 โค b โ 0 < a + b โ (a / (a + b)) โข x + (b / (a + b)) โข y โ s
The theorem `starConvex_iff_div` provides an alternative definition of star-convexity for a set, utilizing division. In the context of this theorem, a set `s` of elements of type `E` is star-convex at a point `x` of the same type if, for any other point `y` in `s` and any two non-negative real numbers `a` and `b` such that their sum is positive, the result of (a / (a + b)) multiplied by `x` plus (b / (a + b)) multiplied by `y` is also a member of `s`. This theorem asserts that this condition is equivalent to the original definition of star-convexity.
More concisely: A set is star-convex at a point if and only if for all points in the set and non-negative real numbers with positive sum, the weighted average of the points belongs to the set.
|
StarConvex.preimage_add_right
theorem StarConvex.preimage_add_right :
โ {๐ : Type u_1} {E : Type u_2} [inst : OrderedSemiring ๐] [inst_1 : AddCommMonoid E] [inst_2 : Module ๐ E]
{x z : E} {s : Set E}, StarConvex ๐ (z + x) s โ StarConvex ๐ x ((fun x => z + x) โปยน' s)
This theorem states that the translation of a star-convex set is also star-convex. In more detail, given a type `๐` with an ordered semiring structure, a type `E` with an addition commutative monoid structure and a module structure over `๐`, and elements `x` and `z` of type `E`, if a set `s` of elements of type `E` is star-convex at a point `z + x`, then the set obtained by translating `s` by `-z` (i.e, the preimage of `s` under the function `x โฆ z + x`) is star-convex at the point `x`.
Star-convexity at a point `x` in a set `s` means that for every point `y` in `s`, and for all nonnegative scalars `a` and `b` such that `a + b = 1`, the point `a โข x + b โข y` is also in `s`, where `a โข x` denotes the scalar multiplication of `a` and `x`, and `+` denotes the addition operation in type `E`.
More concisely: If `s` is a star-convex set at `z + x` in an ordered semiring `๐` with module `E`, then the translated set `{ y : E | z - y โ s }` is star-convex at `x`.
|
starConvex_iff_segment_subset
theorem starConvex_iff_segment_subset :
โ {๐ : Type u_1} {E : Type u_2} [inst : OrderedSemiring ๐] [inst_1 : AddCommMonoid E] [inst_2 : SMul ๐ E] {x : E}
{s : Set E}, StarConvex ๐ x s โ โ โฆy : Eโฆ, y โ s โ segment ๐ x y โ s
The theorem `starConvex_iff_segment_subset` states that for any type `๐` and vector space `E` over `๐` with ordered semiring and additive commutative monoid structures, a set `s` of elements of `E` is star-convex at a point `x` if and only if for every point `y` in `s`, the line segment from `x` to `y` is a subset of `s`. In other words, `s` is star-convex at `x` precisely when any line drawn from `x` to any other point in `s` remains completely within `s`.
More concisely: A set of vectors in a vector space is star-convex at a point if and only if the line segment between that point and any vector in the set is contained within the set.
|
starConvex_iff_pointwise_add_subset
theorem starConvex_iff_pointwise_add_subset :
โ {๐ : Type u_1} {E : Type u_2} [inst : OrderedSemiring ๐] [inst_1 : AddCommMonoid E] [inst_2 : SMul ๐ E] {x : E}
{s : Set E}, StarConvex ๐ x s โ โ โฆa b : ๐โฆ, 0 โค a โ 0 โค b โ a + b = 1 โ a โข {x} + b โข s โ s
This theorem provides an alternative definition of star-convexity of sets in a vector space, in terms of pointwise set operations. A set 's' is star-convex at a point 'x' in the vector space 'E', over an ordered semiring '๐', if and only if for any non-negative scalars 'a' and 'b' that sum to 1, the result of the operation 'a' scaled by the singleton set containing 'x' plus 'b' scaled by 's' is a subset of 's'. In other words, every line segment from 'x' to any point in 's' is wholly contained within 's'.
More concisely: A set 's' in a vector space 'E' over an ordered semiring '๐' is star-convex at a point 'x' if and only if for all non-negative scalars 'a' and 'b' with 'a' + 'b' = 1, 'a' * {x} + 'b' * 's' โ 's'.
|