proposition: Lemma filterI_iter_finI {I : choiceType} T D (f : I -> set T) : finI_from D f = \bigcup_n (filterI_iter (f @` D) n).
proof: Proof. rewrite eqEsubset; split. move=> A [N /= + <-]; have /finite_setP[n] := finite_fset N; elim: n N. move=> ?; rewrite II0 card_eq0 => /eqP -> _; rewrite bigcap_set0. by exists O => //; left. move=> n IH N /eq_cardSP[x Ax + ND]; rewrite -set_fsetD1 => Nxn. have NxD : {subset (N `\ x)%fset <= D}. by move=> ?; rewrite ?inE => /andP [_ /ND /set_mem]. have [r _ xr] := IH _ Nxn NxD; exists r.+1 => //; exists (f x). apply: (@filterI_iter_sub _ _ O) => //; right; exists x => //. by rewrite -inE; apply: ND. exists (\bigcap_(i in [set` (N `\ x)%fset]) f i) => //. by rewrite -bigcap_setU1 set_fsetD1 setD1K. move=> A [n _]; elim: n A. move=> a [-> |[i Di <-]]; [exists fset0 | exists [fset i]%fset] => //. - by rewrite set_fset0 bigcap_set0. - by move=> ?; rewrite !inE => /eqP ->. - by rewrite set_fset1 bigcap_set1. by move=> n IH A /= [B snB [C snC <-]]; apply: finI_fromI; apply: IH. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed