diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-05 15:43:01 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-05 15:43:01 +0000 |
| commit | 14ab34f2e46f7f4b085932347e3f42dd9f0484e4 (patch) | |
| tree | 71335f01e36c53146ff2ef7f4a3476495a54d408 /theories/Reals/Rlimit.v | |
| parent | e1680a9199f3da377beccb3b2b8262b7ae974b33 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2272 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rlimit.v')
| -rw-r--r-- | theories/Reals/Rlimit.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 974c411dc..cf3ba98e0 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -14,6 +14,7 @@ (*********************************************************) Require Export Rbasic_fun. +Require Export R_sqr. Require Export Classical_Prop. Require DiscrR. Require Fourier. @@ -583,6 +584,7 @@ Unfold limit1_in;Unfold limit_in;Simpl;Intros; Save. (*********) +(* Lemma limit_inv : (f:R->R)(D:R->Prop)(l:R)(x0:R) (limit1_in f D l x0)->~(l==R0)->(limit1_in [x:R](Rinv (f x)) D (Rinv l) x0). Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Elim (H ``(Rabsolu l)/2``). Intros delta1 H2; Elim (H ``eps*((Rsqr l)/2)``). @@ -630,3 +632,4 @@ Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption | Change ``0<eps*(Rsqr l)/2``; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Repeat Apply Rmult_lt_pos; [Assumption | Apply Rsqr_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]. Change ``0<(Rabsolu l)/2``; Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]. Save. +*)
\ No newline at end of file |