fact: Definition decomp (A : set rT) : set (set T) := if A == set0 then [set set0] else if pselect (measurable A) is left mA then projT1 (cid (ring_finite_set mA)) else [set A].
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)