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 π]
[add_comm_monoid E]
[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.
theorem
mem_convex_join
{π : Type u_2}
{E : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{s t : set E}
{x : E} :
theorem
convex_join_comm
{π : Type u_2}
{E : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[module π E]
(t : set E) :
convex_join π β
t = β
@[simp]
theorem
convex_join_empty_right
{π : Type u_2}
{E : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(s : set E) :
convex_join π s β
= β
@[simp]
theorem
convex_join_singleton_left
{π : Type u_2}
{E : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(t : set E)
(x : E) :
@[simp]
theorem
convex_join_singleton_right
{π : Type u_2}
{E : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(s : set E)
(y : E) :
@[simp]
theorem
convex_join_singletons
{π : Type u_2}
{E : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_monoid E]
[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 π]
[add_comm_group E]
[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 π]
[add_comm_group E]
[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 π]
[add_comm_group E]
[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 π]
[add_comm_group E]
[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 π]
[add_comm_group E]
[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 π]
[add_comm_group E]
[module π E]
{s : set E}
{x : E}
(hs : s.nonempty) :
β(convex_hull π) (has_insert.insert x s) = convex_join π {x} (β(convex_hull π) s)
theorem
convex_join_segments
{π : Type u_2}
{E : Type u_3}
[linear_ordered_field π]
[add_comm_group E]
[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 π]
[add_comm_group E]
[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 π]
[add_comm_group E]
[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 π]
[add_comm_group E]
[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 π]
[add_comm_group E]
[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 π]
[add_comm_group E]
[module π E]
{s t : set E}
(hs : s.nonempty)
(ht : t.nonempty) :
β(convex_hull π) (s βͺ t) = convex_join π (β(convex_hull π) s) (β(convex_hull π) t)