fact: Definition hull (R : realType) (T : lmodType R) (X : set T) : set T := [set p : T | exists n (g : 'I_n -> T) (d : 'I_n -> R), [/\ (forall i, 0 <= d i)%R, (\sum_(i < n) d i = 1%R), g @` setT `<=` X & p = \sum_(i < n) (d i) *: (g i)] ].
imports: encompass conv mathcomp(all_ssreflect all_algebra vector reals normedtype) mathcomp(classical_sets boolp mathcomp_extra) counterclockwise mathcomp.algebra_tactics(ring) mathcomp.zify(zify)