proposition: Lemma hull_conv_set_strr (p : {prob R}) (X Y : set A) : hull (X :<| p |>: hull Y) = hull (X :<| p |>: Y).
proof: Proof. apply hull_eqEsubset=> u. - case=> x Xx; rewrite conv_pt_setE=> -[] y [] n [] g [] d [] gY yg <-. exists n, (fun i => x <|p|> g i), d; rewrite -ConvnDr yg; split=> //. by move=> v [] i _ <-; exists x=> //; apply/conv_in_conv_pt_set/gY/imageP. - case=> x Xx [] y Yy <-; apply/subset_hull. by exists x=> //; exists y=> //; exact/subset_hull. Qed.
imports: HB(structures) Reals mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets Rstruct reals) mathcomp(finmap) Reals_ext realType_ext classical_sets_ext ssrR fdist fsdist convex