proposition: Lemma eps1''_affine L : affine (@eps1'' L).
proof: Proof. move=> p X Y; rewrite -biglub_conv_setD. congr (|_| _%:ne); apply/neset_ext => /=. by rewrite necset_convType.convE. 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