proposition: Lemma continuity_seq : forall (f:R -> R) (Un:nat -> R) (l:R), continuity_pt f l -> Un_cv Un l -> Un_cv (fun i:nat => f (Un i)) (f l).
proof: Proof. unfold continuity_pt, Un_cv; unfold continue_in. unfold limit1_in. unfold limit_in. unfold dist. simpl. unfold Rdist. intros. elim (H eps H1); intros alp H2. elim H2; intros. elim (H0 alp H3); intros N H5. exists N; intros. case (Req_dec (Un n) l); intro. - rewrite H7; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. - apply H4. split. + unfold D_x, no_cond. split. * trivial. * apply (not_eq_sym (A:=R)); assumption. + apply H5; assumption. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra