segment_eq_image'
theorem segment_eq_image' :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (x y : E),
segment 𝕜 x y = (fun θ => x + θ • (y - x)) '' Set.Icc 0 1
The theorem `segment_eq_image'` states that for any type `𝕜` which is an ordered ring, and any type `E` which is an additive commutative group and a `𝕜`-module, for any two elements `x` and `y` of `E`, the segment between `x` and `y` is equivalent to the image of the function that maps `θ` to `x + θ • (y - x)`, where `θ` ranges over the closed interval from 0 to 1. This theorem is essentially stating that a segment in a vector space between two points can be parameterized by a scalar `θ` in the closed interval [0, 1], where `θ = 0` corresponds to the point `x` and `θ = 1` corresponds to the point `y`.
More concisely: For any ordered ring `𝕜`, additive commutative group and `𝕜`-module `E`, the segment between two elements `x` and `y` in `E` is equal to the image of the function that maps `θ` to `x + θ • (y - x)` for `θ` in the closed interval [0, 1].
|
segment_eq_uIcc
theorem segment_eq_uIcc : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] (x y : 𝕜), segment 𝕜 x y = Set.uIcc x y := by
sorry
The theorem `segment_eq_uIcc` states that for all linear-ordered fields, represented by the symbol 𝕜, and any two elements x and y from this field, the segment between x and y is equivalent to the set of elements lying between x and y, with x and y included. In other words, the set of all combinations of x and y where the coefficients are non-negative and sum to 1 (the definition of a segment) is equal to the set of all elements between the infimum and supremum of x and y (in this case, just x and y themselves because 𝕜 is a linear-ordered field).
More concisely: For any linear-ordered field 𝕜, the segment {x + s * y | x, y ∈ 𝕜, s ∈ ℝ\_+, s * (1 - s) = 1} is equal to the interval [x, y] = {z ∈ 𝕜 | x ≤ z ≤ y}.
|
Convex.mem_Ico
theorem Convex.mem_Ico :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {x y z : 𝕜},
x < y → (z ∈ Set.Ico x y ↔ ∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z)
This theorem states that for any linearly ordered field `𝕜` and any three elements `x`, `y`, and `z` from `𝕜` where `x` is less than `y`, `z` belongs to the left-closed right-open interval `[x, y)` (denoted as `Set.Ico x y`) if and only if there exist two elements `a` and `b` from `𝕜` such that `a` is greater than zero, `b` is non-negative, the sum of `a` and `b` is equal to one, and `z` is equal to the sum of `a` times `x` and `b` times `y`. In other words, `z` lies in the interval `[x, y)` if and only if `z` can be expressed as a semi-strict convex combination of `x` and `y`.
More concisely: For any linearly ordered field `𝕜` and elements `x < y` from `𝕜`, an element `z` belongs to the interval `[x, y)` if and only if there exist `a > 0` and `b ≥ 0` such that `z = a*x + b*y` with `a + b = 1`.
|
openSegment_subset_segment
theorem openSegment_subset_segment :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] (x y : E),
openSegment 𝕜 x y ⊆ segment 𝕜 x y
The theorem `openSegment_subset_segment` states that, for any type `𝕜`, which is an ordered semiring, and for any `E`, which is a type with operations of addition and scalar multiplication, the open segment between two elements `x` and `y` of `E` is a subset of the segment between `x` and `y`. This means every element from the open segment (which includes points represented as a convex combination of `x` and `y` with coefficients strictly between 0 and 1) is also included in the segment (which includes end points `x` and `y`).
More concisely: For any ordered semiring 𝕜 and type E equipped with addition and scalar multiplication, the open segment between any two elements of E (as convex combinations with coefficients in (0,1)) is contained in the closed segment between those elements.
|
openSegment_subset_union
theorem openSegment_subset_union :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
(x y : E) {z : E},
z ∈ Set.range ⇑(AffineMap.lineMap x y) → openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)
This theorem states that for any linearly ordered field `𝕜` and additive commutative group `E` that is a `𝕜`-module, if a point `z` lies on the line segment between points `x` and `y` (expressed as `z ∈ Set.range ⇑(AffineMap.lineMap x y)`), then the open line segment between `x` and `y` (`openSegment 𝕜 x y`) is contained within the union of the open line segments between `x` and `z`, `z` and `y`, and the point `z` itself. In simpler terms, this theorem asserts that the open line segment between two points `x` and `y` can be decomposed into the open line segments between `x` and a point `z` on the line, `z` and `y`, and `z` itself.
More concisely: For any linearly ordered field `𝕜` and `𝕜`-module `E`, if `z` lies on the line segment between `x` and `y` in `E`, then the open line segment between `x` and `y` is contained within the union of the open line segments between `x` and `z`, between `z` and `y`, and at `z`.
|
Convex.mem_Ioo
theorem Convex.mem_Ioo :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {x y z : 𝕜},
x < y → (z ∈ Set.Ioo x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z)
This theorem states that, given a linear ordered field `𝕜` and three elements `x`, `y`, and `z` from that field with `x < y`, a point `z` is in the left-open right-open interval between `x` and `y` if and only if there exist two positive numbers `a` and `b` such that `a` and `b` sum up to 1 and `z` can be expressed as a strict convex combination of `x` and `y`, in other words, `z` equals to `a * x + b * y`.
More concisely: Given a linear ordered field `𝕜` and elements `x`, `y` in `𝕜` with `x < y`, an element `z` lies in the open interval `(x, y)` if and only if there exist `0 < a, b < 1` such that `z = a * x + b * y`.
|
Convex.mem_Ioc
theorem Convex.mem_Ioc :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {x y z : 𝕜},
x < y → (z ∈ Set.Ioc x y ↔ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z)
The theorem `Convex.mem_Ioc` states that for any linear ordered field `𝕜` and any three elements `x`, `y`, and `z` from this field with `x` less than `y`, `z` belongs to the left-open right-closed interval from `x` to `y` if and only if there exist two elements `a` and `b` in `𝕜` satisfying the following four conditions: `a` is nonnegative, `b` is positive, the sum of `a` and `b` equals one, and the sum of `a` times `x` and `b` times `y` equals `z`. In other words, `z` can be expressed as a "semi-strict" convex combination of `x` and `y`.
More concisely: For any linear ordered field and elements x < y, z belongs to the left-open right-closed interval [x, y] if and only if there exist nonnegative a, positive b in the field with a + b = 1 and a*x + b*y = z.
|
segment_eq_image
theorem segment_eq_image :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (x y : E),
segment 𝕜 x y = (fun θ => (1 - θ) • x + θ • y) '' Set.Icc 0 1
This theorem states that for any ordered ring `𝕜` and an additive commutative group `E` that is also a `𝕜`-module, any segment between two points `x` and `y` in `E` is equal to the image of the closed interval [0, 1] under the function that maps each point `θ` to the point `(1 - θ) • x + θ • y`. In simple terms, it provides a parameterization of the line segment between two points in a vector space.
More concisely: For any ordered ring `𝕜` and an additive commutative `𝕜`-module `E`, the segment from `x` to `y` in `E` equals the image of the interval `[0, 1]` under the function `θ ↦ (1 - θ) * x + θ * y`.
|
segment_subset_Icc
theorem segment_subset_Icc :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : OrderedAddCommMonoid E] [inst_2 : Module 𝕜 E]
[inst_3 : OrderedSMul 𝕜 E] {x y : E}, x ≤ y → segment 𝕜 x y ⊆ Set.Icc x y
The theorem `segment_subset_Icc` asserts that for any ordered semiring `𝕜`, any ordered additively commutative monoid `E`, any module `E` over `𝕜`, and any ordered scalar multiplication of `𝕜` and `E`, if `x` and `y` are elements of `E` where `x` is less than or equal to `y`, then the segment from `x` to `y` is a subset of the closed interval `[x, y]`. In simpler terms, the line segment in a vector space from `x` to `y` is contained within the inclusive interval from `x` to `y`, assuming `x` and `y` are ordered such that `x` is less than or equal to `y`.
More concisely: For any ordered semiring 𝕜, ordered additively commutative monoid E with an ordered scalar multiplication, and module E over 𝕜, if x ≤ y in E, then the segment from x to y (inclusive) is contained in the closed interval [x, y].
|
Ioo_subset_openSegment
theorem Ioo_subset_openSegment :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {x y : 𝕜}, Set.Ioo x y ⊆ openSegment 𝕜 x y
This theorem states that for any linearly ordered field `𝕜` and any two elements `x` and `y` of `𝕜`, the left-open right-open interval between `x` and `y` (denoted as `Set.Ioo x y`) is a subset of the open segment between `x` and `y` in the vector space over `𝕜` (denoted as `openSegment 𝕜 x y`). Here, `Set.Ioo x y` is a set of all elements that are strictly greater than `x` and strictly less than `y`, and `openSegment 𝕜 x y` is a set of all points that can be expressed as a non-trivial convex combination of `x` and `y`.
More concisely: For any linearly ordered field `𝕜`, the set of all points that can be expressed as a non-trivial convex combination of two elements `x` and `y` in `𝕜` (`openSegment 𝕜 x y`) is a subset of the set of all elements strictly between `x` and `y` (`Set.Ioo x y`).
|
openSegment_symm
theorem openSegment_symm :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] (x y : E),
openSegment 𝕜 x y = openSegment 𝕜 y x
The theorem `openSegment_symm` states that for any ordered semiring `𝕜` and any two elements `x` and `y` of an additive commutative monoid `E` endowed with a scalar multiplication `SMul` by `𝕜`, the open segment between `x` and `y` is the same as the open segment between `y` and `x`. In other words, the order of `x` and `y` does not matter when determining the open segment, symbolically represented as `openSegment 𝕜 x y = openSegment 𝕜 y x`. An open segment here refers to the set of all points that can be obtained as a convex combination of `x` and `y`, where the coefficients are strictly positive and sum to 1.
More concisely: For any ordered semiring 𝕜 and additive commutative monoid E with scalar multiplication SMul, the open segment between elements x and y in E with respect to 𝕜 is equal to the open segment between y and x.
|
segment_eq_image_lineMap
theorem segment_eq_image_lineMap :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (x y : E),
segment 𝕜 x y = ⇑(AffineMap.lineMap x y) '' Set.Icc 0 1
This theorem states that for any ordered ring `𝕜` and any additive commutative group `E` that is also a `𝕜`-module, and for any two elements `x` and `y` in `E`, the segment between `x` and `y` in `E` is equivalent to the image under the affine map `lineMap` from 0 to 1 (inclusive) in `𝕜`. In simpler terms, all points on the line segment between `x` and `y` can be expressed as affine combinations of `x` and `y` with the coefficients being all real numbers between 0 and 1 inclusive.
More concisely: For any ordered ring `𝕜` and `𝕜`-module `E` that is an additive commutative group, the segment between any two elements `x` and `y` in `E` is equal to the image of the line map from 0 to 1 under the action of `𝕜` in `E`.
|
right_mem_segment
theorem right_mem_segment :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E]
[inst_2 : MulActionWithZero 𝕜 E] (x y : E), y ∈ segment 𝕜 x y
This theorem, named `right_mem_segment`, states that for any ordered semiring `𝕜` and an additive commutative monoid `E` that also allows multiplication by zero, every element `y` in `E` is in the segment between any element `x` and `y` itself. In other words, given any two elements in the vector space (or more generally, in the module), the segment between them always includes the second element. This can be visualized as a line segment on a number line: if you were to draw a line between any two points `x` and `y`, the point `y` is always a part of that line segment.
More concisely: For any ordered semiring 𝕜 and an additive commutative monoid E with multiplication by zero, every element y in E is contained in the segment between any two elements x and y.
|
openSegment_eq_image
theorem openSegment_eq_image :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (x y : E),
openSegment 𝕜 x y = (fun θ => (1 - θ) • x + θ • y) '' Set.Ioo 0 1
This theorem states that for any ordered ring `𝕜` and any additive commutative group `E` that is a `𝕜`-module, and for any two elements `x` and `y` of `E`, the open segment between `x` and `y` is equivalent to the image of the function `(1 - θ) • x + θ • y` over the open interval `(0, 1)`. In simpler terms, every point in the open line segment between `x` and `y` can be represented as a convex combination of `x` and `y` with coefficients in the open interval `(0, 1)`. This theorem is essentially a representation theorem for an open line segment in a vector space.
More concisely: For any ordered ring `𝕜` and `𝕜`-module `E`, the open segment between any two elements `x` and `y` in `E` is equivalent to the image of the function `(1 - θ) • x + θ • y` over the open interval `(0, 1)`, where `θ` is an element of `𝕜` between `0` and `1`.
|
segment_eq_Icc
theorem segment_eq_Icc :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {x y : 𝕜}, x ≤ y → segment 𝕜 x y = Set.Icc x y
The theorem `segment_eq_Icc` states that for any linearly ordered field `𝕜` and any two elements `x` and `y` in this field, if `x` is less than or equal to `y`, then the segment from `x` to `y` is equal to the closed interval from `x` to `y`. In layman's terms, if we take two points on a line, the "segment" between these points (including the points themselves) is exactly the same set of points as the "closed interval" between these points.
More concisely: For any linearly ordered field, the segment between two elements is equal to the closed interval with endpoints at those elements if they are ordered correctly.
|
segment_symm
theorem segment_symm :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] (x y : E),
segment 𝕜 x y = segment 𝕜 y x
This theorem states that for any ordered semiring `𝕜` and any additive commutative monoid `E` with a scalar multiplication operation, the segment from point `x` to point `y` is the same as the segment from point `y` to point `x`. In terms of mathematical notation, a segment is defined as the set of points `z = a*x + b*y`, where `a` and `b` are non-negative and sum to 1. The theorem therefore asserts that this set of points is the same regardless of the order of `x` and `y`.
More concisely: For any ordered semiring `𝕜` and additive commutative monoid `E` with a scalar multiplication operation, the sets of points `{z = a*x + b*y | a, b ∈ 𝕜, a ≥ 0, b ≥ 0, a + b = 1}` and `{z = a*y + b*x | a, b ∈ 𝕜, a ≥ 0, b ≥ 0, a + b = 1}` are equal.
|
left_mem_segment
theorem left_mem_segment :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E]
[inst_2 : MulActionWithZero 𝕜 E] (x y : E), x ∈ segment 𝕜 x y
The theorem `left_mem_segment` states that for any ordered semiring `𝕜`, any additive commutative monoid `E`, and any `𝕜`-zero-preserving scalar multiplication on `E`, for any two elements `x` and `y` in `E`, `x` is an element of the segment between `x` and `y`. In other words, in the context of a vector space, any point `x` is always considered to be on the line segment from `x` to any other point `y`.
More concisely: For any ordered semiring 𝕜, additive commutative monoid E with a 𝕜-zero-preserving scalar multiplication, and any x, y in E, x lies in the segment from x to y.
|
Convex.mem_Icc
theorem Convex.mem_Icc :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {x y z : 𝕜},
x ≤ y → (z ∈ Set.Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z)
The theorem `Convex.mem_Icc` states that for any type `𝕜` which is a linear ordered field and any three elements `x`, `y`, and `z` of this field such that `x` is less than or equal to `y`, `z` is in the closed interval from `x` to `y` (`Set.Icc x y`) if and only if there exist two non-negative numbers `a` and `b` such that the sum of `a` and `b` equals 1 and the weighted sum of `x` and `y` with weights `a` and `b` respectively equals `z`. In other words, `z` is in the interval `[x, y]` if and only if `z` can be expressed as a convex combination of `x` and `y`.
More concisely: For any linear ordered field 𝕜 and elements x, y of 𝕜 with x ≤ y, z is in the closed interval Icc x y if and only if there exist non-negative numbers a, b with a + b = 1 such that z = ax + by.
|