# mathlibdocumentation

analysis.convex.segment

# Segments in vector spaces #

In a π-vector space, we define the following objects and properties.

• segment π x y: Closed segment joining x and y.
• open_segment π 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 open_segment to convex.Icc and convex.Ioo? Should we also define clopen_segment/convex.Ico/convex.Ioc?

def segment (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] (x y : E) :
set E

Segments in a vector space.

Equations
def open_segment (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] (x y : E) :
set E

Open segment in a vector space. Note that open_segment π x x = {x} instead of being β when the base semiring has some element between 0 and 1.

Equations
theorem segment_eq_imageβ (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] (x y : E) :
segment π x y = (Ξ» (p : π Γ π), p.fst β’ x + p.snd β’ y) '' {p : π Γ π | 0 β€ p.fst β§ 0 β€ p.snd β§ p.fst + p.snd = 1}
theorem open_segment_eq_imageβ (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] (x y : E) :
open_segment π x y = (Ξ» (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} [ordered_semiring π] [has_smul π E] (x y : E) :
segment π x y = segment π y x
theorem open_segment_symm (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] (x y : E) :
open_segment π x y = open_segment π y x
theorem open_segment_subset_segment (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] (x y : E) :
open_segment π x y β segment π x y
theorem segment_subset_iff (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_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 open_segment_subset_iff (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] {s : set E} {x y : E} :
open_segment π 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} [ordered_semiring π] [ E] (x y : E) :
x β segment π x y
theorem right_mem_segment (π : Type u_1) {E : Type u_2} [ordered_semiring π] [ E] (x y : E) :
y β segment π x y
@[simp]
theorem segment_same (π : Type u_1) {E : Type u_2} [ordered_semiring π] [module π E] (x : E) :
segment π x x = {x}
theorem insert_endpoints_open_segment (π : Type u_1) {E : Type u_2} [ordered_semiring π] [module π E] (x y : E) :
(open_segment π x y)) = segment π x y
theorem mem_open_segment_of_ne_left_right {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {x y z : E} (hx : x β  z) (hy : y β  z) (hz : z β segment π x y) :
z β open_segment π x y
theorem open_segment_subset_iff_segment_subset {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {s : set E} {x y : E} (hx : x β s) (hy : y β s) :
open_segment π x y β s β segment π x y β s
@[simp]
theorem open_segment_same (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] [nontrivial π] [densely_ordered π] (x : E) :
open_segment π x x = {x}
theorem segment_eq_image (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (x y : E) :
segment π x y = (Ξ» (ΞΈ : π), (1 - ΞΈ) β’ x + ΞΈ β’ y) '' 1
theorem open_segment_eq_image (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (x y : E) :
open_segment π x y = (Ξ» (ΞΈ : π), (1 - ΞΈ) β’ x + ΞΈ β’ y) '' 1
theorem segment_eq_image' (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (x y : E) :
segment π x y = (Ξ» (ΞΈ : π), x + ΞΈ β’ (y - x)) '' 1
theorem open_segment_eq_image' (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (x y : E) :
open_segment π x y = (Ξ» (ΞΈ : π), x + ΞΈ β’ (y - x)) '' 1
theorem segment_eq_image_line_map (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (x y : E) :
segment π x y = β y) '' 1
theorem open_segment_eq_image_line_map (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (x y : E) :
open_segment π x y = β y) '' 1
theorem segment_image (π : Type u_1) {E : Type u_2} {F : Type u_3} [ordered_ring π] [module π E] [module π F] (f : E ββ[π] F) (a b : E) :
βf '' segment π a b = segment π (βf a) (βf b)
@[simp]
theorem open_segment_image (π : Type u_1) {E : Type u_2} {F : Type u_3} [ordered_ring π] [module π E] [module π F] (f : E ββ[π] F) (a b : E) :
βf '' open_segment π a b = open_segment π (βf a) (βf b)
theorem mem_segment_translate (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (a : E) {x b c : E} :
a + x β segment π (a + b) (a + c) β x β segment π b c
@[simp]
theorem mem_open_segment_translate (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (a : E) {x b c : E} :
a + x β open_segment π (a + b) (a + c) β x β open_segment π b c
theorem segment_translate_preimage (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (a b c : E) :
(Ξ» (x : E), a + x) β»ΒΉ' segment π (a + b) (a + c) = segment π b c
theorem open_segment_translate_preimage (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (a b c : E) :
(Ξ» (x : E), a + x) β»ΒΉ' open_segment π (a + b) (a + c) = open_segment π b c
theorem segment_translate_image (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (a b c : E) :
(Ξ» (x : E), a + x) '' segment π b c = segment π (a + b) (a + c)
theorem open_segment_translate_image (π : Type u_1) {E : Type u_2} [ordered_ring π] [module π E] (a b c : E) :
(Ξ» (x : E), a + x) '' open_segment π b c = open_segment π (a + b) (a + c)
theorem same_ray_of_mem_segment {π : Type u_1} {E : Type u_2} [ordered_comm_ring π] [module π E] {x y z : E} (h : x β segment π y z) :
same_ray π (x - y) (z - x)
theorem midpoint_mem_segment {π : Type u_1} {E : Type u_2} [linear_ordered_ring π] [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} [linear_ordered_ring π] [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} [linear_ordered_ring π] [module π E] [invertible 2] (x y : E) :
x β segment π (x + y) (x - y)
@[simp]
theorem left_mem_open_segment_iff {π : Type u_1} {E : Type u_2} [linear_ordered_ring π] [module π E] {x y : E} [densely_ordered π] [ E] :
x β open_segment π x y β x = y
@[simp]
theorem right_mem_open_segment_iff {π : Type u_1} {E : Type u_2} [linear_ordered_ring π] [module π E] {x y : E} [densely_ordered π] [ E] :
y β open_segment π x y β x = y
theorem mem_segment_iff_div {π : Type u_1} {E : Type u_2} [linear_ordered_semifield π] [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_open_segment_iff_div {π : Type u_1} {E : Type u_2} [linear_ordered_semifield π] [module π E] {x y z : E} :
x β open_segment π y z β β (a b : π), 0 < a β§ 0 < b β§ (a / (a + b)) β’ y + (b / (a + b)) β’ z = x
theorem mem_segment_iff_same_ray {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] {x y z : E} :
x β segment π y z β same_ray π (x - y) (z - x)

#### Segments in an ordered space #

Relates segment, open_segment and set.Icc, set.Ico, set.Ioc, set.Ioo

theorem segment_subset_Icc {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] [ordered_smul π E] {x y : E} (h : x β€ y) :
segment π x y β y
theorem open_segment_subset_Ioo {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] [ordered_smul π E] {x y : E} (h : x < y) :
open_segment π x y β y
theorem segment_subset_interval {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] [ordered_smul π E] (x y : E) :
segment π x y β y
theorem convex.min_le_combo {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] [ordered_smul π E] {a b : π} (x y : E) (ha : 0 β€ a) (hb : 0 β€ b) (hab : a + b = 1) :
theorem convex.combo_le_max {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] [ordered_smul π E] {a b : π} (x y : E) (ha : 0 β€ a) (hb : 0 β€ b) (hab : a + b = 1) :
theorem Icc_subset_segment {π : Type u_1} [linear_ordered_field π] {x y : π} :
y β segment π x y
@[simp]
theorem segment_eq_Icc {π : Type u_1} [linear_ordered_field π] {x y : π} (h : x β€ y) :
segment π x y = y
theorem Ioo_subset_open_segment {π : Type u_1} [linear_ordered_field π] {x y : π} :
y β open_segment π x y
@[simp]
theorem open_segment_eq_Ioo {π : Type u_1} [linear_ordered_field π] {x y : π} (h : x < y) :
open_segment π x y = y
theorem segment_eq_Icc' {π : Type u_1} [linear_ordered_field π] (x y : π) :
segment π x y = set.Icc y) y)
theorem open_segment_eq_Ioo' {π : Type u_1} [linear_ordered_field π] {x y : π} (hxy : x β  y) :
open_segment π x y = set.Ioo y) y)
theorem segment_eq_interval {π : Type u_1} [linear_ordered_field π] (x y : π) :
segment π x y = y
theorem convex.mem_Icc {π : Type u_1} [linear_ordered_field π] {x y z : π} (h : x β€ y) :
z β 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} [linear_ordered_field π] {x y z : π} (h : x < y) :
z β 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} [linear_ordered_field π] {x y z : π} (h : x < y) :
z β 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} [linear_ordered_field π] {x y z : π} (h : x < y) :
z β 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.