fact: Definition join1' (s : necset {necset C}) : {convex_set C} := CSet.Pack (CSet.Mixin (hull_is_convex (\bigcup_(x in s) if x \in s then x : set _ else cset0 _))).
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