proposition: Lemma free_semiCompSemiLattConvType_mor'_biglub_morph : biglubmorph free_semiCompSemiLattConvType_mor'.
proof: Proof. move=> /= X; apply necset_ext => /=; rewrite funeqE => b. by rewrite image_preserves_convex_hull bigsetU_affine. 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