proposition: Lemma filter_fromTP {I T : Type} (B : I -> set T) (F : set_system T) : Filter F -> F `=>` filter_from setT B <-> forall i, F (B i).
proof: Proof. by move=> FF; rewrite filter_fromP; split=> [P i|P i _]; apply: P. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed