proposition: Lemma bigsetU_compact I (F : I -> set X) (s : seq I) (P : pred I) : (forall i, P i -> compact (F i)) -> compact (\big[setU/set0]_(i <- s | P i) F i).
proof: Proof. by move=> ?; elim/big_ind : _ =>//; [exact:compact0|exact:compactU]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed