proposition: Lemma finN0_bigcap_closedP T (G : set (set T)) : setI_closed G <-> finN0_bigcap_closed G.
proof: Proof. split=> [GI I D A DF [i Di] GA|GI A B GA GB]; last first. by rewrite -bigcap2inE; apply: GI => // [|[|[|[]]]]; first by exists 0%N. elim/Pchoice: I => I in D DF i Di A GA *. have finDDi : finite_set (D `\ i) by exact: finite_setD. rewrite (bigcap_setD1 i)// -bigsetI_fset_set// big_seq. elim/big_rec: _ => // [|j B]; first by rewrite setIT; apply: GA. rewrite in_fset_set// inE => -[Dj /eqP nij] GAB. by rewrite setICA; apply: GI => //; apply: 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)