proposition: Lemma filter_fromP {I T : Type} (D : set I) (B : I -> set T) (F : set_system T) : Filter F -> F `=>` filter_from D B <-> forall i, D i -> F (B i).
proof: Proof. split; first by move=> FB i ?; apply/FB/in_filter_from. by move=> FB P [i Di BjP]; apply: (filterS BjP); apply: FB. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed