proposition: Lemma bigsetU_affine (X : neset (necset A)) : (f @` (\bigcup_(x in X) x) = \bigcup_(x in free_semiCompSemiLattConvType_mor' @` X) x)%classic.
proof: Proof. rewrite funeqE => b; rewrite propeqE; split. - case => a [x Xx xa] <-{b}. exists (NECSet.Pack (NECSet.Class (CSet.Mixin (is_convex_set_image (Affine.Pack (Affine.Class (isAffine.Axioms_ _ _ (conv_hom_is_affine f)))) x)) (NESet.Mixin (neset_image_neq0 f x)))) => /=; last by exists a. by exists x => //=; exact/necset_ext. - by case => b0 [a0 Xa0 <-{b0}] [a a0a <-{b}]; exists a => //; exists a0. 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