proposition: Lemma continuity_pt_finite_SF : forall (fn:nat -> R -> R) (N:nat) (x:R), (forall n:nat, (n <= N)%nat -> continuity_pt (fn n) x) -> continuity_pt (fun y:R => sum_f_R0 (fun k:nat => fn k y) N) x.
proof: Proof. intros; induction N as [| N HrecN]. - simpl; apply (H 0%nat); apply le_n. - simpl; replace (fun y:R => sum_f_R0 (fun k:nat => fn k y) N + fn (S N) y) with ((fun y:R => sum_f_R0 (fun k:nat => fn k y) N) + (fun y:R => fn (S N) y))%F; [ idtac | reflexivity ]. apply continuity_pt_plus. + apply HrecN. intros; apply H. apply Nat.le_trans with N; [ assumption | apply Nat.le_succ_diag_r ]. + apply (H (S N)); apply le_n. Qed.
imports: Rbase Rfunctions SeqSeries Ranalysis1 MVT Lra