proposition: Lemma uniform_subset_nbhs (f : U -> V) (A B : set U) : B `<=` A -> nbhs (f : {uniform` A -> V}) `=>` nbhs (f : {uniform` B -> V}).
proof: Proof. move => BsubA P /uniform_nbhs [E [entE EsubP]]. apply: (filterS EsubP); apply/uniform_nbhs; exists E; split => //. by move=> h Eh y /BsubA Ay; exact: Eh. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed