proposition: Lemma cvgi_ballP T {F} {FF : Filter F} (f : T -> M -> Prop) y : f `@ F --> y <-> forall eps : R, 0 < eps -> \forall x \near F, exists z, f x z /\ ball y eps z.
proof: Proof. split=> [Fy _/posnumP[eps] |Fy P] /=; first exact/Fy/nbhsx_ballx. move=> /nbhs_ballP[_ /posnumP[eps] subP]. rewrite near_simpl near_mapi; near=> x. have [//|z [fxz yz]] := near (Fy _ (gt0 eps)) x. by exists z => //; split => //; apply: subP. Unshelve. all: end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed