proposition: Lemma __deprecated__cvg_ballPpos {F} {FF : Filter F} (y : M) : F --> y <-> forall eps : {posnum R}, \forall y' \near F, ball y eps%:num y'.
proof: Proof. split => [/fcvg_ballP + eps|pos]; first exact. by apply/fcvg_ballP=> _/posnumP[eps] //. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed