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.

Notations

We provide the following notation:

• [x -[𝕜] y] = segment 𝕜 x y in locale 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} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) (y : E) : Set E

Segments in a vector space.

Equations

• segment 𝕜 x y = {z | ∃ a b x x x, a • x + b • y = z}

def openSegment (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) (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.

Equations

• openSegment 𝕜 x y = {z | ∃ a b x x x, a • x + b • y = z}

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

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

theorem segment_subset_iff (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {x : E} {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} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {x : E} {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} [OrderedSemiring 𝕜] [AddCommMonoid E] [MulActionWithZero 𝕜 E] (x : E) (y : E) : x ∈ segment 𝕜 x y

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

@[simp]

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

theorem insert_endpoints_openSegment (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (x : E) (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} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {y : E} {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} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) : openSegment 𝕜 x y ⊆ s ↔ segment 𝕜 x y ⊆ s

@[simp]

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

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

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

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

theorem openSegment_eq_image' (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (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} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (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} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (y : E) : openSegment 𝕜 x y = ↑(AffineMap.lineMap x y) '' Set.Ioo 0 1

@[simp]

theorem image_segment (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) (a : E) (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} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) (a : E) (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} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup G] [Module 𝕜 E] [AddTorsor G E] [VAddCommClass G E E] (a : G) (b : E) (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} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup G] [Module 𝕜 E] [AddTorsor G E] [VAddCommClass G E E] (a : G) (b : E) (c : E) : a +ᵥ openSegment 𝕜 b c = openSegment 𝕜 (a +ᵥ b) (a +ᵥ c)

@[simp]

theorem mem_segment_translate (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) {x : E} {b : E} {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} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) {x : E} {b : E} {c : E} : a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c

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

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

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

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

theorem segment_inter_eq_endpoint_of_linearIndependent_sub (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {c : E} {x : E} {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} [StrictOrderedCommRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} {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} [OrderedCommRing 𝕜] [NoZeroDivisors 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {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} [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [Invertible 2] (x : E) (y : E) : midpoint 𝕜 x y ∈ segment 𝕜 x y

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

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

@[simp]

theorem left_mem_openSegment_iff {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] : x ∈ openSegment 𝕜 x y ↔ x = y

@[simp]

theorem right_mem_openSegment_iff {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] : y ∈ openSegment 𝕜 x y ↔ x = y

theorem mem_segment_iff_div {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedSemifield 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} {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} [LinearOrderedSemifield 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} {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} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} {z : E} : x ∈ segment 𝕜 y z ↔ SameRay 𝕜 (x - y) (z - x)

theorem openSegment_subset_union {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (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} [OrderedSemiring 𝕜] [OrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x : E} {y : E} (h : x ≤ y) : segment 𝕜 x y ⊆ Set.Icc x y

theorem openSegment_subset_Ioo {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [OrderedCancelAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x : E} {y : E} (h : x < y) : openSegment 𝕜 x y ⊆ Set.Ioo x y

theorem segment_subset_uIcc {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] (x : E) (y : E) : segment 𝕜 x y ⊆ Set.uIcc x y

theorem Convex.min_le_combo {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {a : 𝕜} {b : 𝕜} (x : E) (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} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {a : 𝕜} {b : 𝕜} (x : E) (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} [LinearOrderedField 𝕜] {x : 𝕜} {y : 𝕜} : Set.Icc x y ⊆ segment 𝕜 x y

@[simp]

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

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

@[simp]

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

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

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

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

theorem Convex.mem_Icc {𝕜 : Type u_1} [LinearOrderedField 𝕜] {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} [LinearOrderedField 𝕜] {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} [LinearOrderedField 𝕜] {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} [LinearOrderedField 𝕜] {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 Prod.segment_subset {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x : E × F) (y : E × F) : segment 𝕜 x y ⊆ segment 𝕜 x.fst y.fst ×ˢ segment 𝕜 x.snd y.snd

theorem Prod.openSegment_subset {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x : E × F) (y : E × F) : openSegment 𝕜 x y ⊆ openSegment 𝕜 x.fst y.fst ×ˢ openSegment 𝕜 x.snd y.snd

theorem Prod.image_mk_segment_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x₁ : E) (x₂ : E) (y : F) : (fun x => (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} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x : E) (y₁ : F) (y₂ : F) : (fun y => (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} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x₁ : E) (x₂ : E) (y : F) : (fun x => (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} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x : E) (y₁ : F) (y₂ : F) : (fun y => (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)

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

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

theorem Pi.image_update_segment {𝕜 : Type u_1} {ι : Type u_5} {π : ι → Type u_6} [OrderedSemiring 𝕜] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → Module 𝕜 (π i)] [DecidableEq ι] (i : ι) (x₁ : π i) (x₂ : π i) (y : (i : ι) → π 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} {π : ι → Type u_6} [OrderedSemiring 𝕜] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → Module 𝕜 (π i)] [DecidableEq ι] (i : ι) (x₁ : π i) (x₂ : π i) (y : (i : ι) → π i) : Function.update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (Function.update y i x₁) (Function.update y i x₂)