Convex join #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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)