# Convex hull #

This file defines the convex hull of a set `s` in a module. `convexHull 𝕜 s` is the smallest convex set containing `s`. In order theory speak, this is a closure operator.

## Implementation notes #

`convexHull` is defined as a closure operator. This gives access to the `ClosureOperator` API while the impact on writing code is minimal as `convexHull 𝕜 s` is automatically elaborated as `(convexHull 𝕜) s`.

source
def convexHull (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] :
ClosureOperator (Set E)

The convex hull of a set `s` is the minimal convex set that includes `s`.

Equations

- convexHull 𝕜 = ClosureOperator.ofCompletePred (Convex 𝕜) ⋯

Instances For

source
@[simp]
theorem convexHull_isClosed (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) :
(convexHull 𝕜).IsClosed s = Convex 𝕜 s
source
theorem subset_convexHull (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) :
s ⊆ (convexHull 𝕜) s
source
theorem convex_convexHull (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) :
Convex 𝕜 ((convexHull 𝕜) s)
source
theorem convexHull_eq_iInter (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) :
(convexHull 𝕜) s = ⋂ (t : Set E), ⋂ (_ : s ⊆ t), ⋂ (_ : Convex 𝕜 t), t
source
theorem mem_convexHull_iff {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x : E} :
x ∈ (convexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t
source
theorem convexHull_min {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} :
s ⊆ t → Convex 𝕜 t → (convexHull 𝕜) s ⊆ t
source
theorem Convex.convexHull_subset_iff {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} (ht : Convex 𝕜 t) :
(convexHull 𝕜) s ⊆ t ↔ s ⊆ t
source
theorem convexHull_mono {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} (hst : s ⊆ t) :
(convexHull 𝕜) s ⊆ (convexHull 𝕜) t
source
theorem convexHull_eq_self {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} :
(convexHull 𝕜) s = s ↔ Convex 𝕜 s
source
theorem Convex.convexHull_eq {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} :
Convex 𝕜 s → (convexHull 𝕜) s = s

Alias of the reverse direction of `convexHull_eq_self`.

source
@[simp]
theorem convexHull_univ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] :
(convexHull 𝕜) Set.univ = Set.univ
source
@[simp]
theorem convexHull_empty {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] :
(convexHull 𝕜) ∅ = ∅
source
@[simp]
theorem convexHull_eq_empty {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} :
(convexHull 𝕜) s = ∅ ↔ s = ∅
source
@[deprecated convexHull_eq_empty (since := "2025-08-09")]
theorem convexHull_empty_iff {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} :
(convexHull 𝕜) s = ∅ ↔ s = ∅

Alias of `convexHull_eq_empty`.

source
@[simp]
theorem convexHull_nonempty_iff {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} :
((convexHull 𝕜) s).Nonempty ↔ s.Nonempty
source
theorem Set.Nonempty.convexHull {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} :
s.Nonempty → ((convexHull 𝕜) s).Nonempty

Alias of the reverse direction of `convexHull_nonempty_iff`.

source
theorem segment_subset_convexHull {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
segment 𝕜 x y ⊆ (convexHull 𝕜) s
source
@[simp]
theorem convexHull_singleton {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (x : E) :
(convexHull 𝕜) {x} = {x}
source
@[simp]
theorem convexHull_eq_singleton {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x : E} :
(convexHull 𝕜) s = {x} ↔ s = {x}
source
@[simp]
theorem convexHull_zero {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] :
(convexHull 𝕜) 0 = 0
source
@[simp]
theorem convexHull_eq_zero {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} :
(convexHull 𝕜) s = 0 ↔ s = 0
source
@[simp]
theorem convexHull_pair {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [IsOrderedRing 𝕜] (x y : E) :
(convexHull 𝕜) {x, y} = segment 𝕜 x y
source
theorem convexHull_convexHull_union_left {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s t : Set E) :
(convexHull 𝕜) ((convexHull 𝕜) s ∪ t) = (convexHull 𝕜) (s ∪ t)
source
theorem convexHull_convexHull_union_right {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s t : Set E) :
(convexHull 𝕜) (s ∪ (convexHull 𝕜) t) = (convexHull 𝕜) (s ∪ t)
source
theorem Convex.convex_remove_iff_notMem_convexHull_remove {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (x : E) :
Convex 𝕜 (s \ {x}) ↔ x ∉ (convexHull 𝕜) (s \ {x})
source
@[deprecated Convex.convex_remove_iff_notMem_convexHull_remove (since := "2025-05-23")]
theorem Convex.convex_remove_iff_not_mem_convexHull_remove {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (x : E) :
Convex 𝕜 (s \ {x}) ↔ x ∉ (convexHull 𝕜) (s \ {x})

Alias of `Convex.convex_remove_iff_notMem_convexHull_remove`.

source
theorem IsLinearMap.image_convexHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {f : E → F} (hf : IsLinearMap 𝕜 f) (s : Set E) :
f '' (convexHull 𝕜) s = (convexHull 𝕜) (f '' s)
source
theorem LinearMap.image_convexHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ₗ[𝕜] F) (s : Set E) :
⇑f '' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f '' s)
source
theorem convexHull_add_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} :
(convexHull 𝕜) (s + t) ⊆ (convexHull 𝕜) s + (convexHull 𝕜) t
source
theorem convexHull_smul {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (a : 𝕜) (s : Set E) :
(convexHull 𝕜) (a • s) = a • (convexHull 𝕜) s
source
theorem AffineMap.image_convexHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) (s : Set E) :
⇑f '' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f '' s)
source
theorem convexHull_subset_affineSpan {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) :
(convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)
source
@[simp]
theorem affineSpan_convexHull {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) :
affineSpan 𝕜 ((convexHull 𝕜) s) = affineSpan 𝕜 s
source
theorem convexHull_neg {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) :
(convexHull 𝕜) (-s) = -(convexHull 𝕜) s
source
theorem convexHull_vadd {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (s : Set E) :
(convexHull 𝕜) (x +ᵥ s) = x +ᵥ (convexHull 𝕜) s