proposition: Lemma fin_bigcup_closedP T (G : set (set T)) : (G set0 /\ setU_closed G) <-> fin_bigcup_closed G.
proof: Proof. split=> [[G0 GU] I D A DF GA|GU]; last first. have G0 : G set0 by have := GU void set0 point; rewrite bigcup0//; apply. by split=> // A B GA GB; rewrite -bigcup2inE; apply: GU => // -[|[|[]]]. elim/Pchoice: I => I in D DF A GA *; rewrite -bigsetU_fset_set// big_seq. by elim/big_ind: _ => // i; rewrite in_fset_set// inE => /GA. Qed.
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)