proposition: Lemma filter_finI (T : pointedType) (F : set_system T) (D : set_system T) (f : set T -> set T) : ProperFilter F -> (forall A, D A -> F (f A)) -> finI D f.
proof: Proof. move=> FF sDFf D' sD; apply: (@filter_ex _ F); apply: filter_bigI. by move=> A /sD; rewrite inE => /sDFf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed