proposition: Proposition image_preserves_convex_hull (f : {affine T -> U}) (Z : set T) : f @` (hull Z) = hull (f @` Z).
proof: Proof. rewrite predeqE => b; split. case=> a [n [g [e [Hg]]]] ->{a} <-{b}. exists n, (f \o g), e; split. move=> b /= [i _] <-{b} /=. by exists (g i) => //; apply Hg; exists i. by rewrite Convn_comp. case=> n [g [e [Hg]]] ->{b}. suff [h Hh] : exists h : 'I_n -> T, forall i, Z (h i) /\ f (h i) = g i. exists (<|>_e h). exists n; exists h; exists e; split => //. move=> a [i _] <-. by case: (Hh i). rewrite Convn_comp; apply eq_Convn => // i /=. by case: (Hh i). apply (@fin_all_exists _ _ (fun i hi => Z hi /\ f hi = g i)) => i. case: (Hg (g i)); first by exists i. move=> a // HZa Hfa; by exists a. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist