proposition: Lemma cauchy_ballP (R : numDomainType) (T : pseudoMetricType R) (F : set_system T) (FF : Filter F) : cauchy_ball F <-> cauchy F.
proof: Proof. split=> cauchyF; last first. by move=> _/posnumP[eps]; apply/cauchyF/entourage_ball. move=> U; rewrite -entourage_ballE => - [_/posnumP[eps] xyepsU]. by near do apply: xyepsU; apply: cauchyF. Unshelve. all: by 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