Documentation

Mathlib.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.

source
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.

Equations
Instances For
    source
    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
    source
    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
    source
    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₂
    source
    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
    source
    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₂
    source
    @[simp]
    theorem convexJoin_empty_left {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (t : Set E) :
    convexJoin 𝕜 ∅ t = ∅
    source
    @[simp]
    theorem convexJoin_empty_right {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) :
    convexJoin 𝕜 s ∅ = ∅
    source
    @[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
    source
    @[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
    source
    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
    source
    @[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
    source
    @[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₂
    source
    @[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
    source
    @[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)
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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
    source
    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)
    source
    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)
    source
    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
    source
    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)
    source
    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)
    source
    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}
    source
    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}
    source
    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}