fact: Definition covered_by C P := [set X : set T | exists I D A, [/\ C I D, P I D A & X = \bigcup_(i in D) A 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)