proposition: Lemma cvg_pair {T U V F} {G : set_system U} {H : set_system V} {FF : Filter F} {FG : Filter G} {FH : Filter H} (f : T -> U) (g : T -> V) : f @ F --> G -> g @ F --> H -> (f x, g x) @[x --> F] --> (G, H).
proof: Proof. move=> fFG gFH P; rewrite !near_simpl => -[[A B] /=[GA HB] ABP]; near=> x. by apply: (ABP (_, _)); split=> //=; near: x; [apply: fFG|apply: gFH]. 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