proposition: Lemma uniform_subset_cvg (f : U -> V) (A B : set U) F : Filter F -> B `<=` A -> {uniform A, F --> f} -> {uniform B, F --> f}.
proof: Proof. move => FF /uniform_subset_nbhs => /(_ f). by move=> nbhsF Acvg; apply: cvg_trans; [exact: Acvg|exact: nbhsF]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed