proposition: Lemma fun_complete (F : set_system (T -> U)) {FF : ProperFilter F} : cauchy F -> cvg F.
proof: Proof. move=> Fc. have /(_ _) /cauchy_cvg /cvg_app_entourageP cvF : cauchy (@^~_ @ F). move=> t A /= entA; rewrite near_simpl -near2E near_map2. by apply: Fc; exists A. apply/cvg_ex; exists (fun t => lim (@^~t @ F)). apply/cvg_fct_entourageP => A entA; near=> f => t; near F => g. apply: (entourage_split (g t)) => //; first by near: g; apply: cvF. move: (t); near: g; near: f; apply: nearP_dep; apply: Fc. exists ((split_ent A)^-1)%classic=> //=. 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