proposition: Lemma uniform_entourage : @entourage [the uniformType of {uniform` A -> V}] = filter_from (@entourage V) (fun P => [set fg | forall t : U, A t -> P (fg.1 t, fg.2 t)]).
proof: Proof. rewrite eqEsubset; split => P /=. case=> /= E [F entF FsubE EsubP]; exists F => //; case=> f g Ffg. by apply/EsubP/FsubE=> [[x p]] /=; apply: Ffg; move/set_mem: (p). case=> E entE EsubP; exists [set fg | forall t, E (fg.1 t, fg.2 t)]. by exists E. case=> f g Efg; apply: EsubP => t /mem_set At. by move: Efg => /= /(_ (@exist _ (fun x => in_mem x (mem A)) _ At)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed