proposition: Lemma cvg_within_filter {T U} {f : T -> U} (F : set_system T) {FF : (Filter F) } (G : set_system U) : forall (D : set T), (f @ F) --> G -> (f @ within D F) --> G.
proof: Proof. move=> ?; exact: cvg_trans (cvg_fmap2 (cvg_within _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed