proposition: Lemma closed_bigcup (T : topologicalType) (I : choiceType) (A : set I) (F : I -> set T) : finite_set A -> (forall i, A i -> closed (F i)) -> closed (\bigcup_(i in A) F i).
proof: Proof. move=> finA cF; rewrite -bigsetU_fset_set//; apply: closed_bigsetU => i. by rewrite in_fset_set// inE; exact: cF. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed