proposition: Lemma cvg_fct_entourageP (T : choiceType) (U : uniformType) (F : set_system (T -> U)) (FF : Filter F) (f : T -> U) : F --> f <-> forall A, entourage A -> \forall g \near F, forall t, A (f t, g t).
proof: Proof. split. move=> /cvg_entourageP Ff A entA. by apply: (Ff [set fg | forall t : T, A (fg.1 t, fg.2 t)]); exists A. move=> Ff; apply/cvg_entourageP => A [P entP sPA]. by near=> g do apply: sPA; apply: Ff. 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