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 y : E) : Set E

Segments in a vector space.

Equations

• segment 𝕜 x y = {z : E | ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a • x + b • y = z}

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

Equations

• openSegment 𝕜 x y = {z : E | ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a • x + b • y = z}

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

Segments in a vector space.

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

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

theorem right_mem_segment (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [MulActionWithZero 𝕜 E] (x 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 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 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} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x 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 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 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 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 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 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 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 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 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 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 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 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} [OrderedRing 𝕜] [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} [OrderedRing 𝕜] [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} [OrderedRing 𝕜] [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} [OrderedRing 𝕜] [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} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a b c : E) : (fun (x : E) => 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 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} [StrictOrderedCommRing 𝕜] [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} [OrderedCommRing 𝕜] [NoZeroDivisors 𝕜] [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} [LinearOrderedRing 𝕜] [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} [LinearOrderedRing 𝕜] [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} [LinearOrderedRing 𝕜] [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} [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x 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 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 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} [LinearOrderedSemifield 𝕜] [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} [LinearOrderedField 𝕜] [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} [LinearOrderedField 𝕜] [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} [OrderedSemiring 𝕜] [OrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 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} [OrderedSemiring 𝕜] [OrderedCancelAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 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} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] (x 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 y : E) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : 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 y : E) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • x + b • y ≤ 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 (x ⊓ y) (x ⊔ y)

theorem openSegment_eq_Ioo' {𝕜 : Type u_1} [LinearOrderedField 𝕜] {x y : 𝕜} (hxy : x ≠ y) : openSegment 𝕜 x y = Set.Ioo (x ⊓ y) (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 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} [OrderedSemiring 𝕜] [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} [OrderedSemiring 𝕜] [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} [OrderedSemiring 𝕜] [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} [OrderedSemiring 𝕜] [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} [OrderedSemiring 𝕜] [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} {π : ι → Type u_6} [OrderedSemiring 𝕜] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → Module 𝕜 (π i)] {s : Set ι} (x y : (i : ι) → π i) : segment 𝕜 x y ⊆ s.pi 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 y : (i : ι) → π i) : openSegment 𝕜 x y ⊆ s.pi 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₁ 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₁ x₂ : π i) (y : (i : ι) → π i) : Function.update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (Function.update y i x₁) (Function.update y i x₂)