# 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} [] [] [SMul 𝕜 E] (x : E) (y : E) :
Set E

Segments in a vector space.

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

Segments in a vector space.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem segment_eq_image₂ (𝕜 : Type u_1) {E : Type u_2} [] [] [SMul 𝕜 E] (x : E) (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} [] [] [SMul 𝕜 E] (x : E) (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} [] [] [SMul 𝕜 E] (x : E) (y : E) :
segment 𝕜 x y = segment 𝕜 y x
theorem openSegment_symm (𝕜 : Type u_1) {E : Type u_2} [] [] [SMul 𝕜 E] (x : E) (y : E) :
openSegment 𝕜 x y = openSegment 𝕜 y x
theorem openSegment_subset_segment (𝕜 : Type u_1) {E : Type u_2} [] [] [SMul 𝕜 E] (x : E) (y : E) :
openSegment 𝕜 x y segment 𝕜 x y
theorem segment_subset_iff (𝕜 : Type u_1) {E : Type u_2} [] [] [SMul 𝕜 E] {s : Set E} {x : E} {y : E} :
segment 𝕜 x y s ∀ (a b : 𝕜), 0 a0 ba + b = 1a x + b y s
theorem openSegment_subset_iff (𝕜 : Type u_1) {E : Type u_2} [] [] [SMul 𝕜 E] {s : Set E} {x : E} {y : E} :
openSegment 𝕜 x y s ∀ (a b : 𝕜), 0 < a0 < ba + b = 1a x + b y s
theorem left_mem_segment (𝕜 : Type u_1) {E : Type u_2} [] [] [] (x : E) (y : E) :
x segment 𝕜 x y
theorem right_mem_segment (𝕜 : Type u_1) {E : Type u_2} [] [] [] (x : E) (y : E) :
y segment 𝕜 x y
@[simp]
theorem segment_same (𝕜 : Type u_1) {E : Type u_2} [] [] [Module 𝕜 E] (x : E) :
segment 𝕜 x x = {x}
theorem insert_endpoints_openSegment (𝕜 : Type u_1) {E : Type u_2} [] [] [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} [] [] [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} [] [] [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} [] [] [Module 𝕜 E] [] [] (x : E) :
openSegment 𝕜 x x = {x}
theorem segment_eq_image (𝕜 : Type u_1) {E : Type u_2} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [Module 𝕜 E] (x : E) (y : E) :
segment 𝕜 x y = () '' Set.Icc 0 1
theorem openSegment_eq_image_lineMap (𝕜 : Type u_1) {E : Type u_2} [] [] [Module 𝕜 E] (x : E) (y : E) :
openSegment 𝕜 x y = () '' Set.Ioo 0 1
@[simp]
theorem image_segment (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [] [] [] [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} [] [] [] [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} [] [] [] [Module 𝕜 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} [] [] [] [Module 𝕜 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} [] [] [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} [] [] [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} [] [] [Module 𝕜 E] (a : E) (b : E) (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} [] [] [Module 𝕜 E] (a : E) (b : E) (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} [] [] [Module 𝕜 E] (a : E) (b : E) (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} [] [] [Module 𝕜 E] (a : E) (b : E) (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} [] [] [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} [] [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} [] [] [] [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} [] [Module 𝕜 E] [] (x : E) (y : E) :
midpoint 𝕜 x y segment 𝕜 x y
theorem mem_segment_sub_add {𝕜 : Type u_1} {E : Type u_2} [] [Module 𝕜 E] [] (x : E) (y : E) :
x segment 𝕜 (x - y) (x + y)
theorem mem_segment_add_sub {𝕜 : Type u_1} {E : Type u_2} [] [Module 𝕜 E] [] (x : E) (y : E) :
x segment 𝕜 (x + y) (x - y)
@[simp]
theorem left_mem_openSegment_iff {𝕜 : Type u_1} {E : Type u_2} [] [Module 𝕜 E] {x : E} {y : E} [] [] :
x openSegment 𝕜 x y x = y
@[simp]
theorem right_mem_openSegment_iff {𝕜 : Type u_1} {E : Type u_2} [] [Module 𝕜 E] {x : E} {y : E} [] [] :
y openSegment 𝕜 x y x = y
theorem mem_segment_iff_div {𝕜 : Type u_1} {E : Type u_2} [] [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} [] [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} [] [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} [] [Module 𝕜 E] (x : E) (y : E) {z : E} (hz : z Set.range ()) :
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} [] [Module 𝕜 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} [] [Module 𝕜 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} [] [Module 𝕜 E] [] (x : E) (y : E) :
segment 𝕜 x y Set.uIcc x y
theorem Convex.min_le_combo {𝕜 : Type u_1} {E : Type u_2} [] [Module 𝕜 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} [] [Module 𝕜 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} {x : 𝕜} {y : 𝕜} :
Set.Icc x y segment 𝕜 x y
@[simp]
theorem segment_eq_Icc {𝕜 : Type u_1} {x : 𝕜} {y : 𝕜} (h : x y) :
segment 𝕜 x y = Set.Icc x y
theorem Ioo_subset_openSegment {𝕜 : Type u_1} {x : 𝕜} {y : 𝕜} :
Set.Ioo x y openSegment 𝕜 x y
@[simp]
theorem openSegment_eq_Ioo {𝕜 : Type u_1} {x : 𝕜} {y : 𝕜} (h : x < y) :
openSegment 𝕜 x y = Set.Ioo x y
theorem segment_eq_Icc' {𝕜 : Type u_1} (x : 𝕜) (y : 𝕜) :
segment 𝕜 x y = Set.Icc (min x y) (max x y)
theorem openSegment_eq_Ioo' {𝕜 : Type u_1} {x : 𝕜} {y : 𝕜} (hxy : x y) :
openSegment 𝕜 x y = Set.Ioo (min x y) (max x y)
theorem segment_eq_uIcc {𝕜 : Type u_1} (x : 𝕜) (y : 𝕜) :
segment 𝕜 x y = Set.uIcc x y
theorem Convex.mem_Icc {𝕜 : Type u_1} {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} {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} {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} {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} [] [] [] [Module 𝕜 E] [Module 𝕜 F] (x : E × F) (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} [] [] [] [Module 𝕜 E] [Module 𝕜 F] (x : E × F) (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} [] [] [] [Module 𝕜 E] [Module 𝕜 F] (x₁ : E) (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} [] [] [] [Module 𝕜 E] [Module 𝕜 F] (x : E) (y₁ : F) (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} [] [] [] [Module 𝕜 E] [Module 𝕜 F] (x₁ : E) (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} [] [] [] [Module 𝕜 E] [Module 𝕜 F] (x : E) (y₁ : F) (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} [] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → Module 𝕜 (π i)] {s : Set ι} (x : (i : ι) → π i) (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} [] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → Module 𝕜 (π i)] {s : Set ι} (x : (i : ι) → π i) (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} [] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → Module 𝕜 (π i)] [] (i : ι) (x₁ : π i) (x₂ : π i) (y : (i : ι) → π 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} [] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → Module 𝕜 (π i)] [] (i : ι) (x₁ : π i) (x₂ : π i) (y : (i : ι) → π i) :
'' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (Function.update y i x₁) (Function.update y i x₂)