proposition: Lemma eps1''_biglubmorph L : biglubmorph (@eps1'' L).
proof: Proof. move=> F. transitivity (|_| (biglub @` ((fun X : {necset L} => (X : neset _)) @` F))%:ne). transitivity (|_| (hull (\bigcup_(x in F) x))%:ne). by congr (|_| _); apply neset_ext. by rewrite biglub_hull biglub_bigcup. congr (|_| _). apply/neset_ext; rewrite eqEsubset; split => x [] x0 Fx0 <-. + by case: Fx0 => x1 Fx1 <-; exists x1. + by exists x0 => // ; exists x0. Qed.
imports: Reals mathcomp(all_ssreflect) mathcomp(boolp classical_sets) mathcomp(finmap) infotheo(Reals_ext classical_sets_ext ssrR ssr_ext) infotheo(fdist fsdist convex necset) monae_lib HB(structures) category