proposition: Lemma cvgi_ball T {F} {FF : Filter F} (f : T -> M -> Prop) y : f `@ F --> y -> forall eps : R, 0 < eps -> F [set x | exists z, f x z /\ ball y eps z].
proof: Proof. by move/cvgi_ballP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed