# mathlib3documentation

analysis.convex.join

# 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} [ 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
• s t = (x : E) (H : x s) (y : E) (H : y t), x y
theorem mem_convex_join {𝕜 : Type u_2} {E : Type u_3} [ E] {s t : set E} {x : E} :
x s t (a : E) (H : a s) (b : E) (H : b t), x a b
theorem convex_join_comm {𝕜 : Type u_2} {E : Type u_3} [ E] (s t : set E) :
s t = t s
theorem convex_join_mono {𝕜 : Type u_2} {E : Type u_3} [ E] {s₁ s₂ t₁ t₂ : set E} (hs : s₁ s₂) (ht : t₁ t₂) :
s₁ t₁ s₂ t₂
theorem convex_join_mono_left {𝕜 : Type u_2} {E : Type u_3} [ E] {t s₁ s₂ : set E} (hs : s₁ s₂) :
s₁ t s₂ t
theorem convex_join_mono_right {𝕜 : Type u_2} {E : Type u_3} [ E] {s t₁ t₂ : set E} (ht : t₁ t₂) :
s t₁ s t₂
@[simp]
theorem convex_join_empty_left {𝕜 : Type u_2} {E : Type u_3} [ E] (t : set E) :
t =
@[simp]
theorem convex_join_empty_right {𝕜 : Type u_2} {E : Type u_3} [ E] (s : set E) :
s =
@[simp]
theorem convex_join_singleton_left {𝕜 : Type u_2} {E : Type u_3} [ E] (t : set E) (x : E) :
{x} t = (y : E) (H : y t), x y
@[simp]
theorem convex_join_singleton_right {𝕜 : Type u_2} {E : Type u_3} [ E] (s : set E) (y : E) :
s {y} = (x : E) (H : x s), x y
@[simp]
theorem convex_join_singletons {𝕜 : Type u_2} {E : Type u_3} [ E] {y : E} (x : E) :
{x} {y} = x y
@[simp]
theorem convex_join_union_left {𝕜 : Type u_2} {E : Type u_3} [ E] (s₁ s₂ t : set E) :
(s₁ s₂) t = s₁ t s₂ t
@[simp]
theorem convex_join_union_right {𝕜 : Type u_2} {E : Type u_3} [ E] (s t₁ t₂ : set E) :
s (t₁ t₂) = s t₁ s t₂
@[simp]
theorem convex_join_Union_left {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [ E] (s : ι set E) (t : set E) :
( (i : ι), s i) t = (i : ι), (s i) t
@[simp]
theorem convex_join_Union_right {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [ E] (s : set E) (t : ι set E) :
s ( (i : ι), t i) = (i : ι), s (t i)
theorem segment_subset_convex_join {𝕜 : Type u_2} {E : Type u_3} [ E] {s t : set E} {x y : E} (hx : x s) (hy : y t) :
x y s t
theorem subset_convex_join_left {𝕜 : Type u_2} {E : Type u_3} [ E] {s t : set E} (h : t.nonempty) :
s s t
theorem subset_convex_join_right {𝕜 : Type u_2} {E : Type u_3} [ E] {s t : set E} (h : s.nonempty) :
t s t
theorem convex_join_subset {𝕜 : Type u_2} {E : Type u_3} [ E] {s t u : set E} (hs : s u) (ht : t u) (hu : u) :
s t u
theorem convex_join_subset_convex_hull {𝕜 : Type u_2} {E : Type u_3} [ E] (s t : set E) :
s t (convex_hull 𝕜) (s t)
theorem convex_join_assoc_aux {𝕜 : Type u_2} {E : Type u_3} [ E] (s t u : set E) :
s t) u s t u)
theorem convex_join_assoc {𝕜 : Type u_2} {E : Type u_3} [ E] (s t u : set E) :
s t) u = s t u)
theorem convex_join_left_comm {𝕜 : Type u_2} {E : Type u_3} [ E] (s t u : set E) :
s t u) = t s u)
theorem convex_join_right_comm {𝕜 : Type u_2} {E : Type u_3} [ E] (s t u : set E) :
s t) u = s u) t
theorem convex_join_convex_join_convex_join_comm {𝕜 : Type u_2} {E : Type u_3} [ E] (s t u v : set E) :
s t) u v) = s u) t v)
theorem convex_hull_insert {𝕜 : Type u_2} {E : Type u_3} [ E] {s : set E} {x : E} (hs : s.nonempty) :
(convex_hull 𝕜) s) = {x} ((convex_hull 𝕜) s)
theorem convex_join_segments {𝕜 : Type u_2} {E : Type u_3} [ E] (a b c d : E) :
(segment 𝕜 a b) (segment 𝕜 c d) = (convex_hull 𝕜) {a, b, c, d}
theorem convex_join_segment_singleton {𝕜 : Type u_2} {E : Type u_3} [ E] (a b c : E) :
(segment 𝕜 a b) {c} = (convex_hull 𝕜) {a, b, c}
theorem convex_join_singleton_segment {𝕜 : Type u_2} {E : Type u_3} [ E] (a b c : E) :
{a} (segment 𝕜 b c) = (convex_hull 𝕜) {a, b, c}
@[protected]
theorem convex.convex_join {𝕜 : Type u_2} {E : Type u_3} [ E] {s t : set E} (hs : s) (ht : t) :
s t)
@[protected]
theorem convex.convex_hull_union {𝕜 : Type u_2} {E : Type u_3} [ E] {s t : set E} (hs : s) (ht : t) (hs₀ : s.nonempty) (ht₀ : t.nonempty) :
(convex_hull 𝕜) (s t) = s t
theorem convex_hull_union {𝕜 : Type u_2} {E : Type u_3} [ E] {s t : set E} (hs : s.nonempty) (ht : t.nonempty) :
(convex_hull 𝕜) (s t) = ((convex_hull 𝕜) s) ((convex_hull 𝕜) t)