proposition: Lemma filter_forall T (I : finType) (f : I -> set T) (F : set_system T) : Filter F -> (forall i : I, \forall x \near F, f i x) -> \forall x \near F, forall i, f i x.
proof: Proof. move=> FF fIF; apply: filterS (@filter_bigI T I [fset x in I]%fset f F FF _). by move=> x fIx i; have := fIx i; rewrite /= inE/=; apply. by move=> i; rewrite inE/= => _; apply: (fIF i). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed