proposition: Lemma cvg_mx_entourageP (T : uniformType) m n (F : set_system 'M[T]_(m,n)) (FF : Filter F) (M : 'M[T]_(m,n)) : F --> M <-> forall A, entourage A -> \forall N \near F, forall i j, A (M i j, (N : 'M[T]_(m,n)) i j).
proof: Proof. split. by rewrite filter_fromP => FM A ?; apply: (FM (fun i j => to_set A (M i j))). move=> FM; apply/cvg_entourageP => A [P entP sPA]; near=> N. apply: sPA => /=; near: N; set Q := \bigcap_ij P ij.1 ij.2. apply: filterS (FM Q _); first by move=> N QN i j; apply: (QN _ _ (i, j)). have -> : Q = \bigcap_(ij in [set k | k \in [fset x in predT]%fset]) P ij.1 ij.2. by rewrite predeqE => t; split=> Qt ij _; apply: Qt => //=; rewrite !inE. by apply: filter_bigI => ??; apply: entP. 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