Segments in vector spaces

In a 𝕜-vector space, we define the following objects and properties.

• segment 𝕜 x y: Closed segment joining x and y.
• openSegment 𝕜 x y: Open segment joining x and y.

Notation

We provide the following notation:

• [x -[𝕜] y] = segment 𝕜 x y in scope Convex

TODO

Generalize all this file to affine spaces.

Should we rename segment and openSegment to convex.Icc and convex.Ioo? Should we also define clopenSegment/convex.Ico/convex.Ioc?

def segment (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x y : E) : Set E

Segments in a vector space.

def openSegment (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x y : E) : Set E

Open segment in a vector space. Note that openSegment 𝕜 x x = {x} instead of being ∅ when the base semiring has some element between 0 and 1. Denoted as [x -[𝕜] y] within the Convex namespace.

def Convex.«term[_-[_]_]» : Lean.ParserDescr

Segments in a vector space.

theorem segment_eq_image₂ (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x y : E) : segment 𝕜 x y = (fun (p : 𝕜 × 𝕜) => p.1 • x + p.2 • y) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

theorem openSegment_eq_image₂ (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x y : E) : openSegment 𝕜 x y = (fun (p : 𝕜 × 𝕜) => p.1 • x + p.2 • y) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}

theorem segment_symm (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x y : E) : segment 𝕜 x y = segment 𝕜 y x

theorem openSegment_symm (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x y : E) : openSegment 𝕜 x y = openSegment 𝕜 y x

theorem openSegment_subset_segment (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x y : E) : openSegment 𝕜 x y ⊆ segment 𝕜 x y

theorem segment_subset_iff (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {x y : E} : segment 𝕜 x y ⊆ s ↔ ∀ (a b : 𝕜), 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

theorem openSegment_subset_iff (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {x y : E} : openSegment 𝕜 x y ⊆ s ↔ ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

theorem left_mem_segment (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [ZeroLEOneClass 𝕜] [MulActionWithZero 𝕜 E] (x y : E) : x ∈ segment 𝕜 x y

theorem right_mem_segment (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [ZeroLEOneClass 𝕜] [MulActionWithZero 𝕜 E] (x y : E) : y ∈ segment 𝕜 x y

@[simp]

theorem segment_same (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [ZeroLEOneClass 𝕜] [Module 𝕜 E] (x : E) : segment 𝕜 x x = {x}

theorem insert_endpoints_openSegment (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [ZeroLEOneClass 𝕜] [Module 𝕜 E] (x y : E) : insert x (insert y (openSegment 𝕜 x y)) = segment 𝕜 x y

theorem mem_openSegment_of_ne_left_right {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [ZeroLEOneClass 𝕜] [Module 𝕜 E] {x y z : E} (hx : x ≠ z) (hy : y ≠ z) (hz : z ∈ segment 𝕜 x y) : z ∈ openSegment 𝕜 x y

theorem openSegment_subset_iff_segment_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [ZeroLEOneClass 𝕜] [Module 𝕜 E] {s : Set E} {x y : E} (hx : x ∈ s) (hy : y ∈ s) : openSegment 𝕜 x y ⊆ s ↔ segment 𝕜 x y ⊆ s

theorem segment.lift {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [ZeroLEOneClass 𝕜] [Module 𝕜 E] (R : Type u_7) [Semiring R] [PartialOrder R] [Module R E] [Module R 𝕜] [IsScalarTower R 𝕜 E] [SMulPosMono R 𝕜] (x y : E) : segment R x y ⊆ segment 𝕜 x y

theorem openSegment.lift {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [ZeroLEOneClass 𝕜] [Module 𝕜 E] (R : Type u_7) [Semiring R] [PartialOrder R] [Module R E] [Module R 𝕜] [IsScalarTower R 𝕜 E] [Nontrivial 𝕜] [SMulPosStrictMono R 𝕜] (x y : E) : openSegment R x y ⊆ openSegment 𝕜 x y

@[simp]

theorem openSegment_same (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] [ZeroLEOneClass 𝕜] [Nontrivial 𝕜] [DenselyOrdered 𝕜] (x : E) : openSegment 𝕜 x x = {x}

theorem segment_eq_image (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (x y : E) : segment 𝕜 x y = (fun (θ : 𝕜) => (1 - θ) • x + θ • y) '' Set.Icc 0 1

theorem openSegment_eq_image (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (x y : E) : openSegment 𝕜 x y = (fun (θ : 𝕜) => (1 - θ) • x + θ • y) '' Set.Ioo 0 1

theorem segment_eq_image' (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (x y : E) : segment 𝕜 x y = (fun (θ : 𝕜) => x + θ • (y - x)) '' Set.Icc 0 1

theorem openSegment_eq_image' (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (x y : E) : openSegment 𝕜 x y = (fun (θ : 𝕜) => x + θ • (y - x)) '' Set.Ioo 0 1

theorem segment_eq_image_lineMap (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (x y : E) : segment 𝕜 x y = ⇑(AffineMap.lineMap x y) '' Set.Icc 0 1

theorem openSegment_eq_image_lineMap (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (x y : E) : openSegment 𝕜 x y = ⇑(AffineMap.lineMap x y) '' Set.Ioo 0 1

theorem lineMap_mem_openSegment (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (a b : E) {t : 𝕜} (ht : t ∈ Set.Ioo 0 1) : (AffineMap.lineMap a b) t ∈ openSegment 𝕜 a b

@[simp]

theorem image_segment (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) (a b : E) : ⇑f '' segment 𝕜 a b = segment 𝕜 (f a) (f b)

@[simp]

theorem image_openSegment (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) (a b : E) : ⇑f '' openSegment 𝕜 a b = openSegment 𝕜 (f a) (f b)

@[simp]

theorem vadd_segment (𝕜 : Type u_1) {E : Type u_2} {G : Type u_4} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [AddCommGroup G] [Module 𝕜 E] [AddTorsor G E] [VAddCommClass G E E] (a : G) (b c : E) : a +ᵥ segment 𝕜 b c = segment 𝕜 (a +ᵥ b) (a +ᵥ c)

@[simp]

theorem vadd_openSegment (𝕜 : Type u_1) {E : Type u_2} {G : Type u_4} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [AddCommGroup G] [Module 𝕜 E] [AddTorsor G E] [VAddCommClass G E E] (a : G) (b c : E) : a +ᵥ openSegment 𝕜 b c = openSegment 𝕜 (a +ᵥ b) (a +ᵥ c)

@[simp]

theorem mem_segment_translate (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) {x b c : E} : a + x ∈ segment 𝕜 (a + b) (a + c) ↔ x ∈ segment 𝕜 b c

@[simp]

theorem mem_openSegment_translate (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) {x b c : E} : a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c

theorem segment_translate_preimage (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (a b c : E) : (fun (x : E) => a + x) ⁻¹' segment 𝕜 (a + b) (a + c) = segment 𝕜 b c

theorem openSegment_translate_preimage (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (a b c : E) : (fun (x : E) => a + x) ⁻¹' openSegment 𝕜 (a + b) (a + c) = openSegment 𝕜 b c

theorem segment_translate_image (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (a b c : E) : (fun (x : E) => a + x) '' segment 𝕜 b c = segment 𝕜 (a + b) (a + c)

theorem openSegment_translate_image (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] (a b c : E) : (fun (x : E) => a + x) '' openSegment 𝕜 b c = openSegment 𝕜 (a + b) (a + c)

theorem segment_inter_subset_endpoint_of_linearIndependent_sub (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] {c x y : E} (h : LinearIndependent 𝕜 ![x - c, y - c]) : segment 𝕜 c x ∩ segment 𝕜 c y ⊆ {c}

theorem segment_inter_eq_endpoint_of_linearIndependent_sub (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [AddCommGroup E] [Module 𝕜 E] [ZeroLEOneClass 𝕜] {c x y : E} (h : LinearIndependent 𝕜 ![x - c, y - c]) : segment 𝕜 c x ∩ segment 𝕜 c y = {c}

theorem sameRay_of_mem_segment {𝕜 : Type u_1} {E : Type u_2} [CommRing 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y z : E} (h : x ∈ segment 𝕜 y z) : SameRay 𝕜 (x - y) (z - x)

theorem segment_inter_eq_endpoint_of_linearIndependent_of_ne {𝕜 : Type u_1} {E : Type u_2} [CommRing 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [IsDomain 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y : E} (h : LinearIndependent 𝕜 ![x, y]) {s t : 𝕜} (hs : s ≠ t) (c : E) : segment 𝕜 (c + x) (c + t • y) ∩ segment 𝕜 (c + x) (c + s • y) = {c + x}

theorem midpoint_mem_segment {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [Invertible 2] (x y : E) : midpoint 𝕜 x y ∈ segment 𝕜 x y

theorem mem_segment_sub_add {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [Invertible 2] (x y : E) : x ∈ segment 𝕜 (x - y) (x + y)

theorem mem_segment_add_sub {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [Invertible 2] (x y : E) : x ∈ segment 𝕜 (x + y) (x - y)

@[simp]

theorem left_mem_openSegment_iff {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y : E} [DenselyOrdered 𝕜] [Module.IsTorsionFree 𝕜 E] : x ∈ openSegment 𝕜 x y ↔ x = y

@[simp]

theorem right_mem_openSegment_iff {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y : E} [DenselyOrdered 𝕜] [Module.IsTorsionFree 𝕜 E] : y ∈ openSegment 𝕜 x y ↔ x = y

theorem mem_segment_iff_div {𝕜 : Type u_1} {E : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y z : E} : x ∈ segment 𝕜 y z ↔ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

theorem mem_openSegment_iff_div {𝕜 : Type u_1} {E : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y z : E} : x ∈ openSegment 𝕜 y z ↔ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

theorem mem_segment_iff_sameRay {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y z : E} : x ∈ segment 𝕜 y z ↔ SameRay 𝕜 (x - y) (z - x)

theorem openSegment_subset_union {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (x y : E) {z : E} (hz : z ∈ Set.range ⇑(AffineMap.lineMap x y)) : openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)

If z = lineMap x y c is a point on the line passing through x and y, then the open segment openSegment 𝕜 x y is included in the union of the open segments openSegment 𝕜 x z, openSegment 𝕜 z y, and the point z. Informally, (x, y) ⊆ {z} ∪ (x, z) ∪ (z, y).

Segments in an ordered space

Relates segment, openSegment and Set.Icc, Set.Ico, Set.Ioc, Set.Ioo

theorem segment_subset_Icc {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [PosSMulMono 𝕜 E] {x y : E} (h : x ≤ y) : segment 𝕜 x y ⊆ Set.Icc x y

theorem openSegment_subset_Ioo {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [PartialOrder E] [IsOrderedCancelAddMonoid E] [Module 𝕜 E] [PosSMulStrictMono 𝕜 E] {x y : E} (h : x < y) : openSegment 𝕜 x y ⊆ Set.Ioo x y

theorem segment_subset_uIcc {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [PosSMulMono 𝕜 E] (x y : E) : segment 𝕜 x y ⊆ Set.uIcc x y

theorem Convex.min_le_combo {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [PosSMulMono 𝕜 E] {a b : 𝕜} (x y : E) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : min x y ≤ a • x + b • y

theorem Convex.combo_le_max {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [PosSMulMono 𝕜 E] {a b : 𝕜} (x y : E) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • x + b • y ≤ max x y

theorem Icc_subset_segment {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜} : Set.Icc x y ⊆ segment 𝕜 x y

@[simp]

theorem segment_eq_Icc {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜} (h : x ≤ y) : segment 𝕜 x y = Set.Icc x y

theorem Ioo_subset_openSegment {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜} : Set.Ioo x y ⊆ openSegment 𝕜 x y

@[simp]

theorem openSegment_eq_Ioo {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜} (h : x < y) : openSegment 𝕜 x y = Set.Ioo x y

theorem segment_eq_Icc' {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x y : 𝕜) : segment 𝕜 x y = Set.Icc (min x y) (max x y)

theorem openSegment_eq_Ioo' {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜} (hxy : x ≠ y) : openSegment 𝕜 x y = Set.Ioo (min x y) (max x y)

theorem segment_eq_uIcc {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x y : 𝕜) : segment 𝕜 x y = Set.uIcc x y

theorem Convex.mem_Icc {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y z : 𝕜} (h : x ≤ y) : z ∈ Set.Icc x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Icc iff it can be expressed as a convex combination of the endpoints.

theorem Convex.mem_Ioo {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y z : 𝕜} (h : x < y) : z ∈ Set.Ioo x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ioo iff it can be expressed as a strict convex combination of the endpoints.

theorem Convex.mem_Ioc {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y z : 𝕜} (h : x < y) : z ∈ Set.Ioc x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ioc iff it can be expressed as a semistrict convex combination of the endpoints.

theorem Convex.mem_Ico {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y z : 𝕜} (h : x < y) : z ∈ Set.Ico x y ↔ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ico iff it can be expressed as a semistrict convex combination of the endpoints.

theorem Nonneg.Icc_subset_segment {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : { t : 𝕜 // 0 ≤ t }} : Set.Icc x y ⊆ segment { t : 𝕜 // 0 ≤ t } x y

theorem Nonneg.segment_eq_Icc {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : { t : 𝕜 // 0 ≤ t }} (hxy : x ≤ y) : segment { t : 𝕜 // 0 ≤ t } x y = Set.Icc x y

theorem Nonneg.segment_eq_uIcc {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : { t : 𝕜 // 0 ≤ t }} : segment { t : 𝕜 // 0 ≤ t } x y = Set.uIcc x y

theorem Prod.segment_subset {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x y : E × F) : segment 𝕜 x y ⊆ segment 𝕜 x.1 y.1 ×ˢ segment 𝕜 x.2 y.2

theorem Prod.openSegment_subset {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x y : E × F) : openSegment 𝕜 x y ⊆ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2

theorem Prod.image_mk_segment_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x₁ x₂ : E) (y : F) : (fun (x : E) => (x, y)) '' segment 𝕜 x₁ x₂ = segment 𝕜 (x₁, y) (x₂, y)

theorem Prod.image_mk_segment_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x : E) (y₁ y₂ : F) : (fun (y : F) => (x, y)) '' segment 𝕜 y₁ y₂ = segment 𝕜 (x, y₁) (x, y₂)

theorem Prod.image_mk_openSegment_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x₁ x₂ : E) (y : F) : (fun (x : E) => (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)

@[simp]

theorem Prod.image_mk_openSegment_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x : E) (y₁ y₂ : F) : (fun (y : F) => (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)

theorem Pi.segment_subset {𝕜 : Type u_1} {ι : Type u_5} {M : ι → Type u_6} [Semiring 𝕜] [PartialOrder 𝕜] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module 𝕜 (M i)] {s : Set ι} (x y : (i : ι) → M i) : segment 𝕜 x y ⊆ s.pi fun (i : ι) => segment 𝕜 (x i) (y i)

theorem Pi.openSegment_subset {𝕜 : Type u_1} {ι : Type u_5} {M : ι → Type u_6} [Semiring 𝕜] [PartialOrder 𝕜] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module 𝕜 (M i)] {s : Set ι} (x y : (i : ι) → M i) : openSegment 𝕜 x y ⊆ s.pi fun (i : ι) => openSegment 𝕜 (x i) (y i)

theorem Pi.image_update_segment {𝕜 : Type u_1} {ι : Type u_5} {M : ι → Type u_6} [Semiring 𝕜] [PartialOrder 𝕜] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module 𝕜 (M i)] [DecidableEq ι] (i : ι) (x₁ x₂ : M i) (y : (i : ι) → M i) : Function.update y i '' segment 𝕜 x₁ x₂ = segment 𝕜 (Function.update y i x₁) (Function.update y i x₂)

theorem Pi.image_update_openSegment {𝕜 : Type u_1} {ι : Type u_5} {M : ι → Type u_6} [Semiring 𝕜] [PartialOrder 𝕜] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module 𝕜 (M i)] [DecidableEq ι] (i : ι) (x₁ x₂ : M i) (y : (i : ι) → M i) : Function.update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (Function.update y i x₁) (Function.update y i x₂)