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 convexJoin (𝕜 : Type u_2) {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid 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_convexJoin {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} {x : E} : x ∈ convexJoin 𝕜 s t ↔ ∃ a ∈ s, ∃ b ∈ t, x ∈ segment 𝕜 a b

theorem convexJoin_comm {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s t : Set E) : convexJoin 𝕜 s t = convexJoin 𝕜 t s

theorem convexJoin_mono {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s₁ s₂ t₁ t₂ : Set E} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : convexJoin 𝕜 s₁ t₁ ⊆ convexJoin 𝕜 s₂ t₂

theorem convexJoin_mono_left {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {t s₁ s₂ : Set E} (hs : s₁ ⊆ s₂) : convexJoin 𝕜 s₁ t ⊆ convexJoin 𝕜 s₂ t

theorem convexJoin_mono_right {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t₁ t₂ : Set E} (ht : t₁ ⊆ t₂) : convexJoin 𝕜 s t₁ ⊆ convexJoin 𝕜 s t₂

@[simp]

theorem convexJoin_empty_left {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (t : Set E) : convexJoin 𝕜 ∅ t = ∅

@[simp]

theorem convexJoin_empty_right {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) : convexJoin 𝕜 s ∅ = ∅

@[simp]

theorem convexJoin_singleton_left {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (t : Set E) (x : E) : convexJoin 𝕜 {x} t = ⋃ y ∈ t, segment 𝕜 x y

@[simp]

theorem convexJoin_singleton_right {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (y : E) : convexJoin 𝕜 s {y} = ⋃ x ∈ s, segment 𝕜 x y

theorem convexJoin_singletons {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {y : E} (x : E) : convexJoin 𝕜 {x} {y} = segment 𝕜 x y

@[simp]

theorem convexJoin_union_left {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s₁ s₂ t : Set E) : convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t

@[simp]

theorem convexJoin_union_right {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s t₁ t₂ : Set E) : convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂

@[simp]

theorem convexJoin_iUnion_left {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : ι → Set E) (t : Set E) : convexJoin 𝕜 (⋃ (i : ι), s i) t = ⋃ (i : ι), convexJoin 𝕜 (s i) t

@[simp]

theorem convexJoin_iUnion_right {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t : ι → Set E) : convexJoin 𝕜 s (⋃ (i : ι), t i) = ⋃ (i : ι), convexJoin 𝕜 s (t i)

theorem segment_subset_convexJoin {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} {x y : E} (hx : x ∈ s) (hy : y ∈ t) : segment 𝕜 x y ⊆ convexJoin 𝕜 s t

theorem subset_convexJoin_left {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} [IsOrderedRing 𝕜] (h : t.Nonempty) : s ⊆ convexJoin 𝕜 s t

theorem subset_convexJoin_right {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} [IsOrderedRing 𝕜] (h : s.Nonempty) : t ⊆ convexJoin 𝕜 s t

theorem convexJoin_subset {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t u : Set E} (hs : s ⊆ u) (ht : t ⊆ u) (hu : Convex 𝕜 u) : convexJoin 𝕜 s t ⊆ u

theorem convexJoin_subset_convexHull {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s t : Set E) : convexJoin 𝕜 s t ⊆ (convexHull 𝕜) (s ∪ t)

theorem convexJoin_assoc_aux {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s t u : Set E) : convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)

theorem convexJoin_assoc {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s t u : Set E) : convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u)

theorem convexJoin_left_comm {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s t u : Set E) : convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)

theorem convexJoin_right_comm {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s t u : Set E) : convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t

theorem convexJoin_convexJoin_convexJoin_comm {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s t u v : Set E) : convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)

theorem Convex.convexJoin {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (convexJoin 𝕜 s t)

theorem Convex.convexHull_union {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) (hs₀ : s.Nonempty) (ht₀ : t.Nonempty) : (convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 s t

theorem convexHull_union {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} (hs : s.Nonempty) (ht : t.Nonempty) : (convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 ((convexHull 𝕜) s) ((convexHull 𝕜) t)

theorem convexHull_insert {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} (hs : s.Nonempty) : (convexHull 𝕜) (insert x s) = convexJoin 𝕜 {x} ((convexHull 𝕜) s)

theorem convexJoin_segments {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a b c d : E) : convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜) {a, b, c, d}

theorem convexJoin_segment_singleton {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a b c : E) : convexJoin 𝕜 (segment 𝕜 a b) {c} = (convexHull 𝕜) {a, b, c}

theorem convexJoin_singleton_segment {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a b c : E) : convexJoin 𝕜 {a} (segment 𝕜 b c) = (convexHull 𝕜) {a, b, c}