convex hull of an insert

Stream: Is there code for X?

[Yaël Dillies]

Do we have something akin to this lemma in mathlib? Maybe with affine combinations instead

lemma convex_hull_insert (hA : A.nonempty) :
  convex_hull (insert x A) = ⋃ a ∈ convex_hull A, segment a x :=

The idea is to write an affine combination over A ∪ {x} as the sum of the contribution of x + an affine combination over A.

[Yaël Dillies]

Also, do we have more generally the definition of convex_join : set E → set E → set E such that convex_hull (A ∪ B) = convex_join (convex_hull A) (convex_hull B)?

[Johan Commelin]

@Yury G. Kudryashov I think you are our convexity expert...