# mathlibdocumentation

analysis.convex.join

# Convex join #

This file defines the convex join of two sets. The convex join of s and t is the union of the segments with one end in s and the other in t. This is notably a useful gadget to deal with convex hulls of finite sets.

def convex_join (π : Type u_2) {E : Type u_3} [ordered_semiring π] [module π E] (s t : set E) :
set E

The join of two sets is the union of the segments joining them. This can be interpreted as the topological join, but within the original space.

Equations
theorem mem_convex_join {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] {s t : set E} {x : E} :
x β convex_join π s t β β (a : E) (H : a β s) (b : E) (H : b β t), x β segment π a b
theorem convex_join_comm {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] (s t : set E) :
convex_join π s t = convex_join π t s
theorem convex_join_mono {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] {sβ sβ tβ tβ : set E} (hs : sβ β sβ) (ht : tβ β tβ) :
convex_join π sβ tβ β convex_join π sβ tβ
theorem convex_join_mono_left {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] {t sβ sβ : set E} (hs : sβ β sβ) :
convex_join π sβ t β convex_join π sβ t
theorem convex_join_mono_right {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] {s tβ tβ : set E} (ht : tβ β tβ) :
convex_join π s tβ β convex_join π s tβ
@[simp]
theorem convex_join_empty_left {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] (t : set E) :
@[simp]
theorem convex_join_empty_right {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] (s : set E) :
@[simp]
theorem convex_join_singleton_left {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] (t : set E) (x : E) :
convex_join π {x} t = β (y : E) (H : y β t), segment π x y
@[simp]
theorem convex_join_singleton_right {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] (s : set E) (y : E) :
convex_join π s {y} = β (x : E) (H : x β s), segment π x y
@[simp]
theorem convex_join_singletons {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] {y : E} (x : E) :
convex_join π {x} {y} = segment π x y
@[simp]
theorem convex_join_union_left {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] (sβ sβ t : set E) :
convex_join π (sβ βͺ sβ) t = convex_join π sβ t βͺ convex_join π sβ t
@[simp]
theorem convex_join_union_right {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] (s tβ tβ : set E) :
convex_join π s (tβ βͺ tβ) = convex_join π s tβ βͺ convex_join π s tβ
@[simp]
theorem convex_join_Union_left {ΞΉ : Sort u_1} {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] (s : ΞΉ β set E) (t : set E) :
convex_join π (β (i : ΞΉ), s i) t = β (i : ΞΉ), convex_join π (s i) t
@[simp]
theorem convex_join_Union_right {ΞΉ : Sort u_1} {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] (s : set E) (t : ΞΉ β set E) :
convex_join π s (β (i : ΞΉ), t i) = β (i : ΞΉ), convex_join π s (t i)
theorem segment_subset_convex_join {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] {s t : set E} {x y : E} (hx : x β s) (hy : y β t) :
segment π x y β convex_join π s t
theorem subset_convex_join_left {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] {s t : set E} (h : t.nonempty) :
s β convex_join π s t
theorem subset_convex_join_right {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] {s t : set E} (h : s.nonempty) :
t β convex_join π s t
theorem convex_join_subset {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] {s t u : set E} (hs : s β u) (ht : t β u) (hu : convex π u) :
convex_join π s t β u
theorem convex_join_subset_convex_hull {π : Type u_2} {E : Type u_3} [ordered_semiring π] [module π E] (s t : set E) :
convex_join π s t β β(convex_hull π) (s βͺ t)
theorem convex_join_assoc_aux {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] (s t u : set E) :
convex_join π (convex_join π s t) u β convex_join π s (convex_join π t u)
theorem convex_join_assoc {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] (s t u : set E) :
convex_join π (convex_join π s t) u = convex_join π s (convex_join π t u)
theorem convex_join_left_comm {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] (s t u : set E) :
convex_join π s (convex_join π t u) = convex_join π t (convex_join π s u)
theorem convex_join_right_comm {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] (s t u : set E) :
convex_join π (convex_join π s t) u = convex_join π (convex_join π s u) t
theorem convex_join_convex_join_convex_join_comm {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] (s t u v : set E) :
convex_join π (convex_join π s t) (convex_join π u v) = convex_join π (convex_join π s u) (convex_join π t v)
theorem convex_hull_insert {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] {s : set E} {x : E} (hs : s.nonempty) :
β(convex_hull π) s) = convex_join π {x} (β(convex_hull π) s)
theorem convex_join_segments {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] (a b c d : E) :
convex_join π (segment π a b) (segment π c d) = β(convex_hull π) {a, b, c, d}
theorem convex_join_segment_singleton {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] (a b c : E) :
convex_join π (segment π a b) {c} = β(convex_hull π) {a, b, c}
theorem convex_join_singleton_segment {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] (a b c : E) :
convex_join π {a} (segment π b c) = β(convex_hull π) {a, b, c}
@[protected]
theorem convex.convex_join {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] {s t : set E} (hs : convex π s) (ht : convex π t) :
convex π (convex_join π s t)
@[protected]
theorem convex.convex_hull_union {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] {s t : set E} (hs : convex π s) (ht : convex π t) (hsβ : s.nonempty) (htβ : t.nonempty) :
β(convex_hull π) (s βͺ t) = convex_join π s t
theorem convex_hull_union {π : Type u_2} {E : Type u_3} [linear_ordered_field π] [module π E] {s t : set E} (hs : s.nonempty) (ht : t.nonempty) :
β(convex_hull π) (s βͺ t) = convex_join π (β(convex_hull π) s) (β(convex_hull π) t)