diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 14:10:09 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 14:10:09 +0000 |
| commit | c0ecd40e650b9e8c5b0b0f86c2a6aafde07f41be (patch) | |
| tree | 972edfada3477f9f6cf1cbc2eeb8877fd6104381 /theories/Reals/Rpower.v | |
| parent | d9117de3db059a48e64eda154fa48cf16f8f83c8 (diff) | |
Commentaires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3581 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rpower.v')
| -rw-r--r-- | theories/Reals/Rpower.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 0f213e05e..5ac341355 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -10,8 +10,7 @@ (*i Due to L.Thery i*) (************************************************************) -(* Preuve de l'existence de log et de la fonction puissance *) -(* Propriétés *) +(* Definitions of log and Rpower : R->R->R; main properties *) (************************************************************) Require Rbase. @@ -152,10 +151,10 @@ Assert H3 := (exp_pos x); Red; Intro; Rewrite H4 in H3; Elim (Rlt_antirefl ? H3) Apply Rinv_neq_R0; Red; Intro; Rewrite H3 in H; Elim (Rlt_antirefl ? H). Qed. -(* Définition du log népérien R+*>R *) +(* Definition of log R+* -> R *) Definition Rln [y:posreal] : R := Cases (ln_exists (pos y) (RIneq.cond_pos y)) of (existTT a b) => a end. -(* Une extension sur R *) +(* Extension on R *) Definition ln : R->R := [x:R](Cases (total_order_Rlt R0 x) of (leftT a) => (Rln (mkposreal x a)) | (rightT a) => R0 end). |