proposition: Lemma cvg_uniform_set0 (F : set_system (U -> V)) (f : U -> V) : Filter F -> {uniform set0, F --> f}.
proof: Proof. move=> FF P /= /uniform_nbhs [E [? R]]. suff -> : P = setT by exact: filterT. rewrite eqEsubset; split => //=. by apply: subset_trans R => g _ ?. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed