isExtreme_singleton
theorem isExtreme_singleton :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E]
{A : Set E} {x : E}, IsExtreme 𝕜 A {x} ↔ x ∈ Set.extremePoints 𝕜 A
The theorem `isExtreme_singleton` states that for any ordered semiring type 𝕜, any type E with additive commutative monoid and scalar multiplication, any set A of type E, and any element x of type E, x is an extreme point of A if and only if the singleton set {x} is an extreme subset of A. In other words, the singleton set {x} is considered an extreme subset of A if x only belongs to open segments whose endpoints are within {x}, and this is equivalent to the definition of x being an extreme point of A, which requires that x belongs to no open segment with ends in A, except for the trivial case where the segment is from x to itself.
More concisely: For any ordered semiring type 𝕜, set A of type E with additive commutative monoid and scalar multiplication, and element x in E of type E, x is an extreme point of A if and only if the singleton set {x} is an extreme subset of A.
|
mem_extremePoints_iff_forall_segment
theorem mem_extremePoints_iff_forall_segment :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : LinearOrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : DenselyOrdered 𝕜] [inst_4 : NoZeroSMulDivisors 𝕜 E] {A : Set E} {x : E},
x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
This theorem states that, for any given types `𝕜` and `E` with the respective structures `LinearOrderedRing 𝕜`, `AddCommGroup E`, `Module 𝕜 E`, `DenselyOrdered 𝕜`, and `NoZeroSMulDivisors 𝕜 E`; a set `A` of type `Set E`; and a point `x` of type `E`: `x` is an extreme point of the set `A` if and only if `x` belongs to `A` and for all points `x₁` and `x₂` in `A`, if `x` belongs to the segment from `x₁` to `x₂`, then `x₁` equals `x` or `x₂` equals `x`. In other words, `x` is an extreme point if the only segments that contain it are those with `x` as one of their endpoints.
More concisely: An element $x$ of a densely ordered, linearly ordered ring $E$ with no zero divisors, belonging to a set $A$ of this type, is an extreme point if and only if for all $x\_1, x\_2 \in A$, $x\_1 \leq x \leq x\_2$ or $x\_2 \leq x \leq x\_1$ implies $x\_1 = x$ or $x\_2 = x$.
|
IsExtreme.mem_extremePoints
theorem IsExtreme.mem_extremePoints :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E]
{A : Set E} {x : E}, IsExtreme 𝕜 A {x} → x ∈ Set.extremePoints 𝕜 A
This theorem states that, for any ordered semiring `𝕜`, type `E` with `AddCommMonoid` and `SMul` structures, set `A` of `E` and point `x` of `E`, if the singleton set `{x}` is an extreme subset of `A` (meaning `{x}` is contained in `A` and all points in `{x}` only belong to open segments whose endpoints are in `{x}`), then `x` is an extreme point of `A` (i.e., `x` belongs to no open segment with ends in `A`, except for the trivial open segment from `x` to `x`). The theorem is an alias of the forward direction of `isExtreme_singleton`.
More concisely: If a set `A` in an ordered semiring `𝕜` with an `AddCommMonoid` and `SMul` structure contains the singleton set `{x}` as an extreme subset, then `x` is an extreme point of `A`.
|
extremePoints_subset
theorem extremePoints_subset :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E]
{A : Set E}, Set.extremePoints 𝕜 A ⊆ A
This theorem states that for any ordered semiring `𝕜` and any set `A` of elements of an additive commutative monoid `E` that has a scalar multiplication with `𝕜`, the set of extreme points of `A` is a subset of `A`. In other words, every extreme point of `A` is also an element of `A`. An extreme point `x` of a set `A` is defined as a point that belongs to no open segment with ends in `A`, except for the open segment with both ends at `x`.
More concisely: The set of extreme points of an additive commutative monoid equipped with scalar multiplication by an ordered semiring is a subset of the monoid itself.
|