diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-09 10:52:52 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-09 10:52:52 +0000 |
commit | de54cb8efa08a8bf0cb132d498cbeefad126ab7a (patch) | |
tree | 5316aa075a4d059de86e85177002c55aec846181 /theories/Reals/Ranalysis1.v | |
parent | 326a261ee30daa035716908fa0b89e1cfe056c14 (diff) |
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"
Expérience avec les notations et les scopes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3876 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Ranalysis1.v')
-rw-r--r-- | theories/Reals/Ranalysis1.v | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index b4c2c8cce..2b883f7b6 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -12,7 +12,8 @@ Require Rbase. Require Rfunctions. Require Export Rlimit. Require Export Rderiv. -Import R_scope. +V7only [Import R_scope.]. +Implicit Variable Type f:R->R. (****************************************************) (** Basic operations on functions *) @@ -27,6 +28,19 @@ Definition div_real_fct [a:R;f:R->R] : R->R := [x:R] ``a/(f x)``. Definition comp [f1,f2:R->R] : R->R := [x:R] ``(f1 (f2 x))``. Definition inv_fct [f:R->R] : R->R := [x:R]``/(f x)``. +Infix "+" plus_fct (at level 4, left associativity) : Rfun_scope. +Notation "- x" := (opp_fct x) (at level 0) : Rfun_scope + V8only (at level 40). +Infix "*" mult_fct (at level 3, left associativity) : Rfun_scope. +Infix "-" minus_fct (at level 4, left associativity) : Rfun_scope. +Infix "/" div_fct (at level 3, left associativity) : Rfun_scope. +Notation "f1 'o' f2" := (comp f1 f2) (at level 2, right associativity) + : Rfun_scope. +Notation "/ x" := (inv_fct x) (at level 0): Rfun_scope + V8only (at level 30, left associativity). + +Delimits Scope Rfun_scope with F. + Definition fct_cte [a:R] : R->R := [x:R]a. Definition id := [x:R]x. @@ -53,6 +67,8 @@ Definition constant_D_eq [f:R->R;D:R->Prop;c:R] : Prop := (x:R) (D x) -> (f x)== Definition continuity_pt [f:R->R; x0:R] : Prop := (continue_in f no_cond x0). Definition continuity [f:R->R] : Prop := (x:R) (continuity_pt f x). +Arguments Scope continuity_pt [Rfun_scope R_scope]. +Arguments Scope continuity [Rfun_scope]. (**********) Lemma continuity_pt_plus : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (plus_fct f1 f2) x0). @@ -181,6 +197,13 @@ Definition derivable [f:R->R] := (x:R)(derivable_pt f x). Definition derive_pt [f:R->R;x:R;pr:(derivable_pt f x)] := (projT1 ? ? pr). Definition derive [f:R->R;pr:(derivable f)] := [x:R](derive_pt f x (pr x)). +Arguments Scope derivable_pt_lim [Rfun_scope R_scope]. +Arguments Scope derivable_pt_abs [Rfun_scope R_scope R_scope]. +Arguments Scope derivable_pt [Rfun_scope R_scope]. +Arguments Scope derivable [Rfun_scope]. +Arguments Scope derive_pt [Rfun_scope R_scope _]. +Arguments Scope derive [Rfun_scope _]. + Definition antiderivative [f,g:R->R;a,b:R] : Prop := ((x:R)``a<=x<=b``->(EXT pr : (derivable_pt g x) | (f x)==(derive_pt g x pr)))/\``a<=b``. (************************************) (** Class of differential functions *) |