proposition: Lemma continuity_pt_comp : forall f1 f2 (x:R), continuity_pt f1 x -> continuity_pt f2 (f1 x) -> continuity_pt (f2 o f1) x.
proof: Proof. unfold continuity_pt; unfold continue_in; intros; unfold comp. cut (limit1_in (fun x0:R => f2 (f1 x0)) (Dgf (D_x no_cond x) (D_x no_cond (f1 x)) f1) ( f2 (f1 x)) x -> limit1_in (fun x0:R => f2 (f1 x0)) (D_x no_cond x) (f2 (f1 x)) x). - intro; apply H1. eapply limit_comp. + apply H. + apply H0. - unfold limit1_in; unfold limit_in; unfold dist; simpl; unfold Rdist; intros. assert (H3 := H1 eps H2). elim H3; intros. exists x0. split. + elim H4; intros; assumption. + intros; case (Req_dec (f1 x) (f1 x1)); intro. * rewrite H6; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. * elim H4; intros; apply H8. split. -- unfold Dgf, D_x, no_cond. split. ++ split. ** trivial. ** elim H5; unfold D_x, no_cond; intros. elim H9; intros; assumption. ++ split. ** trivial. ** assumption. -- elim H5; intros; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv