proposition: Proposition preimage_preserves_convex_hull (f : {linear T -> U}) (Z : set U) : Z `<=` range f -> f @^-1` (hull Z) = hull (f @^-1` Z).
proof: Proof. rewrite eqEsubset=>Zf; split; last by apply preimage_subset_convex_hull. move=>x [n [g [d [gZ fx]]]]. move: Zf=>/(subset_trans gZ)/factorize_range [h ge]; subst g. rewrite -preimage_add_ker hull_add. exists (<|>_d h). by exists n, h, d; split=>// y [z _ <-] /=; apply gZ; exists z. exists (x - <|>_d h). by apply subset_hull=>/=; rewrite linearB Convn_comp fx subrr. by rewrite addrC -addrA [-_+_]addrC subrr addr0. 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