proposition: Lemma cvgi_comp T U V (f : T -> U) (g : U -> set V) (F : set_system T) (G : set_system U) (H : set_system V) : f @ F `=>` G -> g `@ G `=>` H -> g \o f `@ F `=>` H.
proof: Proof. by move=> fFG gGH; apply: cvg_trans gGH => P /fFG. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed