proposition: Lemma uniform_limit_continuous {U : topologicalType} {V : uniformType} (F : set_system (U -> V)) (f : U -> V) : ProperFilter F -> (\forall g \near F, continuous (g : U -> V)) -> {uniform, F --> f} -> continuous f.
proof: Proof. move=> PF ctsF Ff x; apply/cvg_app_entourageP => A entA; near F => g; near=> y. apply: (entourage_split (g x)) => //. by near: g; apply/Ff/uniform_nbhs; exists (split_ent A); split => // ?; exact. apply: (entourage_split (g y)) => //; near: y; near: g. by apply: (filterS _ ctsF) => g /(_ x) /cvg_app_entourageP; exact. apply/Ff/uniform_nbhs; exists (split_ent (split_ent A))^-1%classic. by split; [exact: entourage_inv | move=> g fg; near_simpl; near=> z; exact: fg]. Unshelve. all: 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