proposition: Lemma biglub_necset_bigsetU (I : Type) (S : neset I) (F : I -> neset (necset A)) : biglub_necset (bignesetU S F) = biglub_necset (biglub_necset @` (F @` S))%:ne.
proof: Proof. apply necset_ext => /=. apply: hull_eqEsubset => a. - case => x [] i Si Fix xa. exists 1, (fun _ => a), (fdist1 ord0). split; last by rewrite ConvnI1E. move=> a0 [] zero _ <-. exists (biglub_necset (F i)); first by do 2 apply imageP. by apply/subset_hull; exists x. - case => x [] u [] i Si Fiu <-. case => n [] g [] d [] /= gx ag. exists n, g, d; split => //. apply: (subset_trans gx). move => a0 [] x0 ux0 x0a0. exists x0 => //; exists i => //. by rewrite Fiu. 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