proposition: Lemma free_semiCompSemiLattConvType_mor'_affine : affine free_semiCompSemiLattConvType_mor'.
proof: Proof. move=> p a0 a1; apply necset_ext => /=; rewrite predeqE => b0; split. - rewrite !necset_convType.convE. case=> a [] a0' a0a0'; rewrite conv_pt_setE=> -[] a1' a1a1' <- <- /=. by rewrite affine_conv /=; exact: conv_in_conv_set. - rewrite !necset_convType.convE. move=> /conv_in_conv_set' [] x [] y [] [] a0' a0a0' <- [] [] a1' a1a1' <- ->. rewrite affine_image_conv_set /=. by apply conv_in_conv_set; apply imageP. 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