fact: Definition finite_subset_cover (I : choiceType) (D : set I) U (F : I -> set U) (A : set U) := exists2 D' : {fset I}, {subset D' <= D} & A `<=` cover [set` D'] F.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed