proposition: Lemma eps0_Dist1 (A : Type) (d : P_delta_acto A) : eps0 _ (fsdist1 d) = d.
proof: Proof. by rewrite eps0E Convn_of_fsdist1. 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