proposition: Lemma unif_continuousP (U V : pseudoMetricType R) (f : U -> V) : unif_continuous f <-> forall e, e > 0 -> exists2 d, d > 0 & forall x, ball x.1 d x.2 -> ball (f x.1) e (f x.2).
proof: Proof. have fappF : Filter ((fun xy => (f xy.1, f xy.2)) @ entourage_ ball). by rewrite entourage_ballE; apply: fmap_filter. by rewrite /unif_continuous -!entourage_ballE filter_fromP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed