fact: Definition cauchy_ball {R : numDomainType} {T : pseudoMetricType R} (F : set_system T) := forall e, e > 0 -> \forall x & y \near F, ball x e y.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed