proposition: Lemma fam_nbhs {U : choiceType} {V : uniformType} (fam : set U -> Prop) (A : set U) (E : set (V * V)) (f : {family fam, U -> V}) : entourage E -> fam A -> nbhs f [set g | forall y, A y -> E (f y, g y)].
proof: Proof. move=> entE famA; have /fam_cvgP /(_ A) : (nbhs f --> f) by []; apply => //. by apply uniform_nbhs; exists E; split. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed