proposition: Lemma continuous2_cvg {T : Type} {V W U : topologicalType} (F : set_system T) (FF : Filter F) (f : T -> V) (g : T -> W) (h : V -> W -> U) (a : V) (b : W) : h z.1 z.2 @[z --> (a, b)] --> h a b -> f @ F --> a -> g @ F --> b -> (fun x => h (f x) (g x)) @ F --> h a b.
proof: Proof. move=> h_continuous fa fb; apply: (cvg_trans _ h_continuous). exact: (@cvg_comp _ _ _ _ (fun x => h x.1 x.2) _ _ _ (cvg_pair fa fb)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed