proposition: Lemma continuity_sum (I : finType) F (P : pred I): (forall i, P i -> continuity (F i)) -> continuity (fun x => (\sum_(i | P i) ((F i) x)))%R.
proof: Proof. move=> H; elim: (index_enum I)=> [|a l IHl]. set f:= fun _ => _. have Hf: (fun x=> 0) =1 f by move=> x; rewrite /f big_nil. by apply: (continuity_eq Hf); exact: continuity_const. set f := fun _ => _. case Hpa: (P a). have Hf: (fun x => F a x + \sum_(i <- l | P i) F i x)%R =1 f. by move=> x; rewrite /f big_cons Hpa. apply: (continuity_eq Hf); apply: continuity_plus=> //. exact: H. have Hf: (fun x => \sum_(i <- l | P i) F i x)%R =1 f. by move=> x; rewrite /f big_cons Hpa. exact: (continuity_eq Hf). Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun Zwf Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def Rtrigo1 Reals mathcomp(all_ssreflect ssralg poly mxpoly ssrnum) HB(structures)