proposition: Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) (F : set (set T)) (P : set T) : Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) -> F ([set j | P j -> (\bigcap_(i in [set` D]) f i) j]).
proof: Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed