proposition: Lemma continuous'_imp_continuous : forall (A B : CPsMetricSpace) (f : CSetoid_fun A B), continuous' f -> continuous f.
proof: Proof. intros A B f. unfold continuous' in |- *. intro H. unfold continuous in |- *. intros x n H0. elim H with x (power n 2). intros p H1. exists (S p). intros y H2. apply leEq_less_trans with (one_div_succ (R:=IR) (power n 2)). apply H1. apply less_leEq. apply less_transitive_unfolded with (([1][/] Two:IR[//]H0)[^]S p). exact H2. unfold one_div_succ in |- *. astepl (OneR[^]S p[/] (Two:IR)[^]S p[//]nexp_resp_ap_zero (S p) H0). astepl (OneR[/] (Two:IR)[^]S p[//]nexp_resp_ap_zero (S p) H0). apply recip_resp_less. unfold Snring in |- *. apply nring_pos. intuition. apply nat_less_bin_nexp. unfold one_div_succ in |- *. unfold Snring in |- *. astepr (OneR[^]n[/] (Two:IR)[^]n[//]nexp_resp_ap_zero n H0). astepr (OneR[/] (Two:IR)[^]n[//]nexp_resp_ap_zero n H0). apply recip_resp_less. apply nexp_resp_pos. apply pos_two. astepr (nring (R:=IR) (power n 2)[+][1]). astepl (nexp IR n Two[+][0]). apply plus_resp_leEq_less. apply eq_imp_leEq. apply nexp_power. apply pos_one. Qed.
imports: CoRN.metrics.CPseudoMSpaces