proposition: Lemma uniform_nbhsT (f : U -> V) : (nbhs (f : {uniform U -> V})) = nbhs (f : [the topologicalType of U -> V]).
proof: Proof. rewrite eqEsubset; split=> A. case/uniform_nbhs => E [entE] /filterS; apply. exists [set fh | forall y, E (fh.1 y, fh.2 y)]; first by exists E. by move=> ? /=. case => J [E entE EJ] /filterS; apply; apply/uniform_nbhs; exists E. by split => // z /= Efz; apply: EJ => t /=; exact: Efz. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed