proposition: Lemma mx_complete (F : set_system 'M[T]_(m, n)) : ProperFilter F -> cauchy F -> cvg F.
proof: Proof. move=> FF Fc. have /(_ _ _) /cauchy_cvg /cvg_app_entourageP cvF : cauchy ((fun M : 'M[T]_(m, n) => M _ _) @ F). move=> i j A /= entA; rewrite near_simpl -near2E near_map2. by apply: Fc; exists (fun _ _ => A). apply/cvg_ex. set Mlim := \matrix_(i, j) (lim ((fun M : 'M[T]_(m, n) => M i j) @ F) : T). exists Mlim; apply/cvg_mx_entourageP => A entA; near=> M => i j; near F => M'. apply: subset_split_ent => //; exists (M' i j) => /=. by near: M'; rewrite mxE; apply: cvF. move: (i) (j); near: M'; near: M; apply: nearP_dep; apply: Fc. by exists (fun _ _ => (split_ent A)^-1%classic) => ?? //; apply: entourage_inv. 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