# mathlib3documentation

analysis.convex.segment

# Segments in vector spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

## 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
@[simp]
theorem image_segment (π : 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 image_open_segment (π : 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)
@[simp]
theorem vadd_segment (π : Type u_1) {E : Type u_2} {G : Type u_4} [ordered_ring π] [module π E] [ E] [ E] (a : G) (b c : E) :
a +α΅₯ segment π b c = segment π (a +α΅₯ b) (a +α΅₯ c)
@[simp]
theorem vadd_open_segment (π : Type u_1) {E : Type u_2} {G : Type u_4} [ordered_ring π] [module π E] [ E] [ E] (a : G) (b c : E) :
a +α΅₯ open_segment π b c = open_segment π (a +α΅₯ b) (a +α΅₯ c)
@[simp]
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} [strict_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)
theorem open_segment_subset_union {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (x y : E) {z : E} (hz : z β ) :
open_segment π x y β (open_segment π x z βͺ open_segment π z y)

If z = line_map x y c is a point on the line passing through x and y, then the open segment open_segment π x y is included in the union of the open segments open_segment π x z, open_segment π z y, and the point z. Informally, (x, y) β {z} βͺ (x, z) βͺ (z, y).

#### 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_uIcc {π : 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_uIcc {π : 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.

theorem prod.segment_subset {π : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π] [module π E] [module π F] (x y : E Γ F) :
segment π x y β segment π x.fst y.fst ΓΛ’ segment π x.snd y.snd
theorem prod.open_segment_subset {π : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π] [module π E] [module π F] (x y : E Γ F) :
open_segment π x y β open_segment π x.fst y.fst ΓΛ’ open_segment π x.snd y.snd
theorem prod.image_mk_segment_left {π : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π] [module π E] [module π F] (xβ xβ : E) (y : F) :
(Ξ» (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} [ordered_semiring π] [module π E] [module π F] (x : E) (yβ yβ : F) :
(Ξ» (y : F), (x, y)) '' segment π yβ yβ = segment π (x, yβ) (x, yβ)
theorem prod.image_mk_open_segment_left {π : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π] [module π E] [module π F] (xβ xβ : E) (y : F) :
(Ξ» (x : E), (x, y)) '' open_segment π xβ xβ = open_segment π (xβ, y) (xβ, y)
@[simp]
theorem prod.image_mk_open_segment_right {π : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π] [module π E] [module π F] (x : E) (yβ yβ : F) :
(Ξ» (y : F), (x, y)) '' open_segment π yβ yβ = open_segment π (x, yβ) (x, yβ)
theorem pi.segment_subset {π : Type u_1} {ΞΉ : Type u_5} {Ο : ΞΉ β Type u_6} [ordered_semiring π] [Ξ  (i : ΞΉ), add_comm_monoid (Ο i)] [Ξ  (i : ΞΉ), module π (Ο i)] {s : set ΞΉ} (x y : Ξ  (i : ΞΉ), Ο i) :
segment π x y β s.pi (Ξ» (i : ΞΉ), segment π (x i) (y i))
theorem pi.open_segment_subset {π : Type u_1} {ΞΉ : Type u_5} {Ο : ΞΉ β Type u_6} [ordered_semiring π] [Ξ  (i : ΞΉ), add_comm_monoid (Ο i)] [Ξ  (i : ΞΉ), module π (Ο i)] {s : set ΞΉ} (x y : Ξ  (i : ΞΉ), Ο i) :
open_segment π x y β s.pi (Ξ» (i : ΞΉ), open_segment π (x i) (y i))
theorem pi.image_update_segment {π : Type u_1} {ΞΉ : Type u_5} {Ο : ΞΉ β Type u_6} [ordered_semiring π] [Ξ  (i : ΞΉ), add_comm_monoid (Ο i)] [Ξ  (i : ΞΉ), module π (Ο i)] [decidable_eq ΞΉ] (i : ΞΉ) (xβ xβ : Ο i) (y : Ξ  (i : ΞΉ), Ο i) :
'' segment π xβ xβ = segment π i xβ) i xβ)
theorem pi.image_update_open_segment {π : Type u_1} {ΞΉ : Type u_5} {Ο : ΞΉ β Type u_6} [ordered_semiring π] [Ξ  (i : ΞΉ), add_comm_monoid (Ο i)] [Ξ  (i : ΞΉ), module π (Ο i)] [decidable_eq ΞΉ] (i : ΞΉ) (xβ xβ : Ο i) (y : Ξ  (i : ΞΉ), Ο i) :
'' open_segment π xβ xβ = open_segment π i xβ) i xβ)