diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-24 10:27:08 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-24 10:27:08 +0000 |
| commit | 38734c5e122e9a38cf5b8afc586f47abced11361 (patch) | |
| tree | 2227afa958bf809d9152b526e29f183b552e5e61 /theories/Reals/SeqSeries.v | |
| parent | c69ae2a1f05db124c19b7f326ca23e980f643198 (diff) | |
changement de pose en set (pose n'etait pas utilise avec la semantique
documentee).
Reste a retablir la semantique de pose.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
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 2c035cf83..602cd871b 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; |