diff options
Diffstat (limited to 'theories/Reals/SeqSeries.v')
| -rw-r--r-- | theories/Reals/SeqSeries.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 2c035cf837..602cd871b4 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -281,7 +281,7 @@ assert (H5 := cv_infty_cv_R0 _ H4 H1); assert (H6 : 0 < eps / 2)... unfold Rdiv in |- *; apply Rmult_lt_0_compat... apply Rinv_0_lt_compat; prove_sup... elim (H _ H6); clear H; intros N1 H; - pose (C := Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1)); + set (C := Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1)); assert (H7 : exists N : nat, @@ -309,7 +309,7 @@ ring... discrR... apply Rabs_no_R0... apply Rabs_no_R0... -elim H7; clear H7; intros N2 H7; pose (N := max N1 N2); exists (S N); intros; +elim H7; clear H7; intros N2 H7; set (N := max N1 N2); exists (S N); intros; unfold R_dist in |- *; replace (sum_f_R0 (fun k:nat => An k * Bn k) n / sum_f_R0 An n - l) with (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n / sum_f_R0 An n)... @@ -375,7 +375,7 @@ Lemma Cesaro_1 : forall (An:nat -> R) (l:R), Un_cv An l -> Un_cv (fun n:nat => sum_f_R0 An (pred n) / INR n) l. Proof with trivial. -intros Bn l H; pose (An := fun _:nat => 1)... +intros Bn l H; set (An := fun _:nat => 1)... assert (H0 : forall n:nat, 0 < An n)... intro; unfold An in |- *; apply Rlt_0_1... assert (H1 : forall n:nat, 0 < sum_f_R0 An n)... @@ -385,7 +385,7 @@ unfold cv_infty in |- *; intro; case (Rle_dec M 0); intro... exists 0%nat; intros; apply Rle_lt_trans with 0... assert (H2 : 0 < M)... auto with real... -clear n; pose (m := up M); elim (archimed M); intros; +clear n; set (m := up M); elim (archimed M); intros; assert (H5 : (0 <= m)%Z)... apply le_IZR; unfold m in |- *; simpl in |- *; left; apply Rlt_trans with M... elim (IZN _ H5); intros; exists x; intros; unfold An in |- *; rewrite sum_cte; |