proposition: Lemma uniform_nbhs (f : {uniform` A -> V}) P: nbhs f P <-> (exists E, entourage E /\ [set h | forall y, A y -> E(f y, h y)] `<=` P).
proof: Proof. split=> [[Q [[/= W oW <- /=] Wf subP]]|[E [entE subP]]]. rewrite openE /= /interior in oW. case: (oW _ Wf) => ? [ /= E entE] Esub subW. exists E; split=> // h Eh; apply/subP/subW/Esub => /= [[u Au]]. by apply: Eh => /=; rewrite -inE. near=> g; apply: subP => y /mem_set Ay; rewrite -!(sigLE A). move: (SigSub _); near: g. have := (@cvg_image _ _ (@sigL _ V A) _ f (nbhs_filter f) (image_sigL point)).1 cvg_id [set h | forall y, E (sigL A f y, h y)]. case; first by exists [set fg | forall y, E (fg.1 y, fg.2 y)]; [exists E|]. move=> B nbhsB rBrE; apply: (filterS _ nbhsB) => g Bg [y yA]. by move: rBrE; rewrite eqEsubset; case => [+ _]; apply; exists g. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed