proposition: Lemma cvg_app_within {T} {U : topologicalType} (f : T -> U) (F : set_system T) (D : set T): Filter F -> cvg (f @ F) -> cvg (f @ within D F).
proof: Proof. by move => FF /cvg_ex [l H]; apply/cvg_ex; exists l; exact: cvg_within_filter. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed