proposition: Lemma bigfcup_imfset (T I : choiceType) (P : {fset I}) (f : I -> T) : \bigcup_(x <- P) [fset f x] = f @` P.
proof: Proof. apply/eqP; rewrite eqEfsubset; apply/andP; split; apply/fsubsetP=> x. - case/bigfcupP=> i /andP [] iP _. rewrite inE => /eqP ->. by apply/imfsetP; exists i. - case/imfsetP => i /= iP ->; apply/bigfcupP; exists i; rewrite ?andbT //. by apply/imfsetP; exists (f i); rewrite ?inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(finmap) Reals mathcomp(mathcomp_extra) mathcomp(classical_sets boolp cardinality Rstruct reals) mathcomp(ereal topology esum measure probability) ssrR realType_ext Reals_ext ssr_ext ssralg_ext bigop_ext fdist convex