mathlib documentation

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.

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.

Equations
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} :
x ∈ convex_join π•œ s t ↔ βˆƒ (a : E) (H : a ∈ s) (b : E) (H : b ∈ t), x ∈ segment π•œ a b
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) :
@[simp]
theorem convex_join_empty_right {π•œ : Type u_2} {E : Type u_3} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (s : set E) :
@[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) :
convex_join π•œ {x} t = ⋃ (y : E) (H : y ∈ t), segment π•œ x y
@[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) :
convex_join π•œ s {y} = ⋃ (x : E) (H : x ∈ s), segment π•œ x y
@[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)