proposition: Lemma eps1_correct (s : necset {necset C}) : @eps1 _ s = join1 s.
proof: Proof. rewrite eps1E; apply/necset_ext => /=; congr (hull _). rewrite /bigcup; rewrite funeqE => c; rewrite propeqE; split. - by case=> X sX Xc; exists X => //; rewrite -in_setE in sX; rewrite sX. - case=> X sX; rewrite -in_setE in sX; rewrite sX => Xc; exists X => //. by rewrite -in_setE. 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