proposition: Lemma is_convex_set_preimage [T U : convType] (f : {affine T -> U}) (A : {convex_set U}) : is_convex_set (f @^-1` A)%classic.
proof: Proof. apply/asboolP=>x y p/= Ax Ay. by rewrite affine_conv -in_setE; apply/mem_convex_set; rewrite in_setE. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals