proposition: Lemma continuous_mult {U : UniformSpace} {K : AbsRing} (f g : U -> K) (x : U) : continuous f x -> continuous g x -> continuous (fun y => mult (f y) (g y)) x.
proof: Proof. intros. by eapply filterlim_comp_2, filterlim_mult. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq