diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:46:36 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:46:36 +0000 |
| commit | 9aeaac7698c670cc7ac92dd53cd674b5b321aab3 (patch) | |
| tree | b02945c21c26e6c67d0e17175bfb0e3f52b89f5c /theories/Reals/Rcomplete.v | |
| parent | 096310efb4266fe89455d473f704ec6c7ed5a97c (diff) | |
Modifications dans SeqProp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3590 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rcomplete.v')
| -rw-r--r-- | theories/Reals/Rcomplete.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index 8a653d1aa..0fff7c42a 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -24,8 +24,8 @@ Require Max. Theorem R_complete : (Un:nat->R) (Cauchy_crit Un) -> (sigTT R [l:R](Un_cv Un l)). Intros. -Pose Vn := (suite_minorant Un (cauchy_min Un H)). -Pose Wn := (suite_majorant Un (cauchy_maj Un H)). +Pose Vn := (sequence_minorant Un (cauchy_min Un H)). +Pose Wn := (sequence_majorant Un (cauchy_maj Un H)). Assert H0 := (maj_cv Un H). Fold Wn in H0. Assert H1 := (min_cv Un H). @@ -126,7 +126,7 @@ Replace ``-(x-(Wn N))`` with ``(Wn N)-x``; [Apply H4 | Ring]. Unfold ge N. Apply le_trans with (max N1 N2); Apply le_max_l. Unfold Wn Vn. -Unfold suite_majorant suite_minorant. +Unfold sequence_majorant sequence_minorant. Assert H7 := (approx_maj [k:nat](Un (plus N k)) (maj_ss Un N (cauchy_maj Un H))). Assert H8 := (approx_min [k:nat](Un (plus N k)) (min_ss Un N (cauchy_min Un H))). Cut (Wn N)==(majorant ([k:nat](Un (plus N k))) (maj_ss Un N (cauchy_maj Un H))). |