proposition: Lemma is_convex_set_image (f : {affine T -> U}) (a : {convex_set T}) : is_convex_set (f @` a).
proof: Proof. rewrite /is_convex_set. apply/asboolP => x y p [a0 Ha0 <-{x}] [a1 Ha1 <-{y}]. exists (a0 <|p|> a1); last by rewrite affine_conv. by rewrite -in_setE; apply/mem_convex_set; rewrite in_setE. 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