# mathlib3documentation

analysis.convex.hull

# Convex hull #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the convex hull of a set s in a module. convex_hull π s is the smallest convex set containing s. In order theory speak, this is a closure operator.

## Implementation notes #

convex_hull is defined as a closure operator. This gives access to the closure_operator API while the impact on writing code is minimal as convex_hull π s is automatically elaborated as β(convex_hull π) s.

def convex_hull (π : Type u_1) {E : Type u_2} [ordered_semiring π] [module π E] :

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

Equations
theorem subset_convex_hull (π : Type u_1) {E : Type u_2} [ordered_semiring π] [module π E] (s : set E) :
s β β(convex_hull π) s
theorem convex_convex_hull (π : Type u_1) {E : Type u_2} [ordered_semiring π] [module π E] (s : set E) :
convex π (β(convex_hull π) s)
theorem convex_hull_eq_Inter (π : Type u_1) {E : Type u_2} [ordered_semiring π] [module π E] (s : set E) :
β(convex_hull π) s = β (t : set E) (hst : s β t) (ht : convex π t), t
theorem mem_convex_hull_iff {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {s : set E} {x : E} :
x β β(convex_hull π) s β β (t : set E), s β t β convex π t β x β t
theorem convex_hull_min {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {s t : set E} (hst : s β t) (ht : convex π t) :
β(convex_hull π) s β t
theorem convex.convex_hull_subset_iff {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {s t : set E} (ht : convex π t) :
theorem convex_hull_mono {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {s t : set E} (hst : s β t) :
β(convex_hull π) s β β(convex_hull π) t
theorem convex.convex_hull_eq {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {s : set E} (hs : convex π s) :
β(convex_hull π) s = s
@[simp]
theorem convex_hull_univ {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] :
@[simp]
theorem convex_hull_empty {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] :
@[simp]
theorem convex_hull_empty_iff {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {s : set E} :
@[simp]
theorem convex_hull_nonempty_iff {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {s : set E} :
@[protected]
theorem set.nonempty.convex_hull {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {s : set E} :

Alias of the reverse direction of convex_hull_nonempty_iff.

theorem segment_subset_convex_hull {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {s : set E} {x y : E} (hx : x β s) (hy : y β s) :
segment π x y β β(convex_hull π) s
@[simp]
theorem convex_hull_singleton {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] (x : E) :
β(convex_hull π) {x} = {x}
@[simp]
theorem convex_hull_zero {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] :
β(convex_hull π) 0 = 0
@[simp]
theorem convex_hull_pair {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] (x y : E) :
β(convex_hull π) {x, y} = segment π x y
theorem convex_hull_convex_hull_union_left {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] (s t : set E) :
β(convex_hull π) (β(convex_hull π) s βͺ t) = β(convex_hull π) (s βͺ t)
theorem convex_hull_convex_hull_union_right {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] (s t : set E) :
β(convex_hull π) (s βͺ β(convex_hull π) t) = β(convex_hull π) (s βͺ t)
theorem convex.convex_remove_iff_not_mem_convex_hull_remove {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] {s : set E} (hs : convex π s) (x : E) :
convex π (s \ {x}) β x β β(convex_hull π) (s \ {x})
theorem is_linear_map.convex_hull_image {π : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π] [module π E] [module π F] {f : E β F} (hf : is_linear_map π f) (s : set E) :
β(convex_hull π) (f '' s) = f '' β(convex_hull π) s
theorem linear_map.convex_hull_image {π : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π] [module π E] [module π F] (f : E ββ[π] F) (s : set E) :
β(convex_hull π) (βf '' s) = βf '' β(convex_hull π) s
theorem convex_hull_smul {π : Type u_1} {E : Type u_2} [ordered_comm_semiring π] [module π E] (a : π) (s : set E) :
β(convex_hull π) (a β’ s) = a β’ β(convex_hull π) s
theorem affine_map.image_convex_hull {π : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring π] [module π E] [module π F] (s : set E) (f : E βα΅[π] F) :
βf '' β(convex_hull π) s = β(convex_hull π) (βf '' s)
theorem convex_hull_subset_affine_span {π : Type u_1} {E : Type u_2} [ordered_ring π] [module π E] (s : set E) :
β(convex_hull π) s β β(affine_span π s)
@[simp]
theorem affine_span_convex_hull {π : Type u_1} {E : Type u_2} [ordered_ring π] [module π E] (s : set E) :
affine_span π (β(convex_hull π) s) = affine_span π s
theorem convex_hull_neg {π : Type u_1} {E : Type u_2} [ordered_ring π] [module π E] (s : set E) :
β(convex_hull π) (-s) = -β(convex_hull π) s