proposition: Lemma continuous_comp_2 {U V W X : UniformSpace} (f : U -> V) (g : U -> W) (h : V -> W -> X) (x : U) : continuous f x -> continuous g x -> continuous (fun (x : V * W) => h (fst x) (snd x)) (f x,g x) -> continuous (fun x => h (f x) (g x)) x.
proof: Proof. intros Cf Cg Ch. eapply filterlim_comp_2. by apply Cf. by apply Cg. apply filterlim_locally => eps. case: (proj1 (filterlim_locally _ _) Ch eps) => /= del Hdel. rewrite {1}/ball /= /prod_ball /= in Hdel. exists (fun y => ball (f x) (pos del) y) (fun y => ball (g x) (pos del) y). apply locally_ball. apply locally_ball. move => y z /= Hy Hz. apply (Hdel (y,z)). by split. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq