proposition: Lemma pointwise_cvg_entourage (x : X) (f : {ptws X -> Y}) E : entourage E -> \forall g \near f, E (f x, g x).
proof: Proof. move=> entE; have : ({ptws, nbhs f --> f}) by []. rewrite pointwise_cvg_family_singleton => /fam_cvgP /(_ [set x]). rewrite uniform_set1 => /(_ _ (to_set E (f x))); apply; first by exists x. by move: E entE; exact/cvg_entourageP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed