proposition: Lemma uniform_set1 F (f : U -> V) (x : U) : Filter F -> {uniform [set x], F --> f} = (g x @[g --> F] --> f x).
proof: Proof. move=> FF; rewrite propeqE; split. move=> + W => /(_ [set t | W (t x)]) +; rewrite -nbhs_entourageE. rewrite uniform_nbhs => + [Q entQ subW]. by apply; exists Q; split => // h Qf; exact/subW/Qf. move=> Ff W; rewrite uniform_nbhs => [[E] [entE subW]]. apply: (filterS subW); move/(nbhs_entourage (f x))/Ff: entE => //=; near_simpl. by apply: filter_app; apply: nearW=> ? ? ? ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed