proposition: Lemma filter_bigI T (I : choiceType) (D : {fset I}) (f : I -> set T) (F : set_system T) : Filter F -> (forall i, i \in D -> F (f i)) -> F (\bigcap_(i in [set` D]) f i).
proof: Proof. move=> FF FfD. suff: F [set p | forall i, i \in enum_fset D -> f i p] by []. have {FfD} : forall i, i \in enum_fset D -> F (f i) by move=> ? /FfD. elim: (enum_fset D) => [|i s ihs] FfD; first exact: filterS filterT. apply: (@filterS _ _ _ (f i `&` [set p | forall i, i \in s -> f i p])). by move=> p [fip fsp] j; rewrite inE => /orP [/eqP->|] //; apply: fsp. apply: filterI; first by apply: FfD; rewrite inE eq_refl. by apply: ihs => j sj; apply: FfD; rewrite inE sj orbC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed