proposition: Lemma cvg_comp2 {T U V W} {F : set_system T} {G : set_system U} {H : set_system V} {I : set_system W} {FF : Filter F} {FG : Filter G} {FH : Filter H} (f : T -> U) (g : T -> V) (h : U -> V -> W) : f @ F --> G -> g @ F --> H -> h (fst x) (snd x) @[x --> (G, H)] --> I -> h (f x) (g x) @[x --> F] --> I.
proof: Proof. by move=> fFG gFH hGHI P /= IP; apply: cvg_pair (hGHI _ IP). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed