proposition: Lemma eq_in_close (A : set U) (f g : {uniform` A -> V}) : {in A, f =1 g} -> close f g.
proof: Proof. rewrite entourage_close => /eq_sigLP eqfg ? [E entE]; apply=> /=. by rewrite /map_pair eqfg; exact: entourage_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed