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.

source

def convexJoin (𝕜 : Type u_2) {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (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.

Instances For

source

theorem mem_convexJoin {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} {x : E} :

x ∈ convexJoin 𝕜 s t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ x ∈ segment 𝕜 a b

source

theorem convexJoin_comm {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t : Set E) :

convexJoin 𝕜 s t = convexJoin 𝕜 t s

source

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

convexJoin 𝕜 s₁ t₁ ⊆ convexJoin 𝕜 s₂ t₂

source

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

convexJoin 𝕜 s₁ t ⊆ convexJoin 𝕜 s₂ t

source

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

convexJoin 𝕜 s t₁ ⊆ convexJoin 𝕜 s t₂

source

@[simp]

theorem convexJoin_empty_left {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (t : Set E) :

convexJoin 𝕜 ∅ t = ∅

source

@[simp]

theorem convexJoin_empty_right {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) :

convexJoin 𝕜 s ∅ = ∅

source

@[simp]

theorem convexJoin_singleton_left {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (t : Set E) (x : E) :

convexJoin 𝕜 {x} t = ⋃ (y : E) (_ : y ∈ t), segment 𝕜 x y

source

@[simp]

theorem convexJoin_singleton_right {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (y : E) :

convexJoin 𝕜 s {y} = ⋃ (x : E) (_ : x ∈ s), segment 𝕜 x y

source

theorem convexJoin_singletons {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {y : E} (x : E) :

convexJoin 𝕜 {x} {y} = segment 𝕜 x y

source

@[simp]

theorem convexJoin_union_left {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s₁ : Set E) (s₂ : Set E) (t : Set E) :

convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t

source

@[simp]

theorem convexJoin_union_right {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t₁ : Set E) (t₂ : Set E) :

convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂

source

@[simp]

theorem convexJoin_iUnion_left {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : ι → Set E) (t : Set E) :

convexJoin 𝕜 (⋃ (i : ι), s i) t = ⋃ (i : ι), convexJoin 𝕜 (s i) t

source

@[simp]

theorem convexJoin_iUnion_right {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t : ι → Set E) :

convexJoin 𝕜 s (⋃ (i : ι), t i) = ⋃ (i : ι), convexJoin 𝕜 s (t i)

source

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

segment 𝕜 x y ⊆ convexJoin 𝕜 s t

source

theorem subset_convexJoin_left {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} (h : Set.Nonempty t) :

s ⊆ convexJoin 𝕜 s t

source

theorem subset_convexJoin_right {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} (h : Set.Nonempty s) :

t ⊆ convexJoin 𝕜 s t

source

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

convexJoin 𝕜 s t ⊆ u

source

theorem convexJoin_subset_convexHull {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t : Set E) :

convexJoin 𝕜 s t ⊆ ↑(convexHull 𝕜) (s ∪ t)

source

theorem convexJoin_assoc_aux {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (t : Set E) (u : Set E) :

convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)

source

theorem convexJoin_assoc {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (t : Set E) (u : Set E) :

convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u)

source

theorem convexJoin_left_comm {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (t : Set E) (u : Set E) :

convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)

source

theorem convexJoin_right_comm {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (t : Set E) (u : Set E) :

convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t

source

theorem convexJoin_convexJoin_convexJoin_comm {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (t : Set E) (u : Set E) (v : Set E) :

convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)

source

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

Convex 𝕜 (convexJoin 𝕜 s t)

source

theorem Convex.convexHull_union {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) (hs₀ : Set.Nonempty s) (ht₀ : Set.Nonempty t) :

↑(convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 s t

source

theorem convexHull_union {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} (hs : Set.Nonempty s) (ht : Set.Nonempty t) :

↑(convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 (↑(convexHull 𝕜) s) (↑(convexHull 𝕜) t)

source

theorem convexHull_insert {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} (hs : Set.Nonempty s) :

↑(convexHull 𝕜) (insert x s) = convexJoin 𝕜 {x} (↑(convexHull 𝕜) s)

source

theorem convexJoin_segments {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) (b : E) (c : E) (d : E) :

convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = ↑(convexHull 𝕜) {a, b, c, d}

source

theorem convexJoin_segment_singleton {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) (b : E) (c : E) :

convexJoin 𝕜 (segment 𝕜 a b) {c} = ↑(convexHull 𝕜) {a, b, c}

source

theorem convexJoin_singleton_segment {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) (b : E) (c : E) :

convexJoin 𝕜 {a} (segment 𝕜 b c) = ↑(convexHull 𝕜) {a, b, c}