fact: Definition sigma_subadditive {T} {R : numFieldType} (mu : set T -> \bar R) := forall (F : (set T) ^nat), mu (\bigcup_n (F n)) <= \sum_(i <oo) mu (F i).
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)