diff options
Diffstat (limited to 'theories/Reals/Rlimit.v')
| -rw-r--r-- | theories/Reals/Rlimit.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 658ffd12f..3d52a98cd 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -164,7 +164,7 @@ Definition limit_in (X X':Metric_Space) (f:Base X -> Base X') eps > 0 -> exists alp : R, alp > 0 /\ - (forall x:Base X, D x /\ dist X x x0 < alp -> dist X' (f x) l < eps). + (forall x:Base X, D x /\ X.(dist) x x0 < alp -> X'.(dist) (f x) l < eps). (*******************************) (** ** R is a metric space *) @@ -191,9 +191,9 @@ Lemma tech_limit : Proof. intros f D l x0 H H0. case (Rabs_pos (f x0 - l)); intros H1. - absurd (dist R_met (f x0) l < dist R_met (f x0) l). + absurd (R_met.(@dist) (f x0) l < R_met.(@dist) (f x0) l). apply Rlt_irrefl. - case (H0 (dist R_met (f x0) l)); auto. + case (H0 (R_met.(@dist) (f x0) l)); auto. intros alpha1 [H2 H3]; apply H3; auto; split; auto. case (dist_refl R_met x0 x0); intros Hr1 Hr2; rewrite Hr2; auto. case (dist_refl R_met (f x0) l); intros Hr1 Hr2; symmetry; auto. @@ -345,8 +345,9 @@ Lemma single_limit : adhDa D x0 -> limit1_in f D l x0 -> limit1_in f D l' x0 -> l = l'. Proof. unfold limit1_in; unfold limit_in; intros. + simpl in *. cut (forall eps:R, eps > 0 -> dist R_met l l' < 2 * eps). - clear H0 H1; unfold dist; unfold R_met; unfold R_dist; + clear H0 H1; simpl @dist; unfold R_met; unfold R_dist, dist; unfold Rabs; case (Rcase_abs (l - l')); intros. cut (forall eps:R, eps > 0 -> - (l - l') < eps). intro; generalize (prop_eps (- (l - l')) H1); intro; @@ -356,7 +357,7 @@ Proof. intros; cut (eps * / 2 > 0). intro; generalize (H0 (eps * / 2) H2); rewrite (Rmult_comm eps (/ 2)); rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2). - elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial. + elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial. apply (Rlt_dichotomy_converse 2 0); right; generalize Rlt_0_1; intro; unfold Rgt; generalize (Rplus_lt_compat_l 1 0 1 H3); intro; elim (Rplus_ne 1); intros a b; rewrite a in H4; |