X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FExponential.ma;h=434241caaee2a242bc72a486633fd3c2c8e09039;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=8a1b637c641393e60ccf9ed9da0409d40ae15495;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/Exponential.ma b/helm/software/matita/contribs/CoRN-Decl/transc/Exponential.ma index 8a1b637c6..434241caa 100644 --- a/helm/software/matita/contribs/CoRN-Decl/transc/Exponential.ma +++ b/helm/software/matita/contribs/CoRN-Decl/transc/Exponential.ma @@ -16,11 +16,11 @@ set "baseuri" "cic:/matita/CoRN-Decl/transc/Exponential". +include "CoRN.ma". + (* $Id: Exponential.v,v 1.7 2004/04/23 10:01:07 lcf Exp $ *) -(* INCLUDE -TaylorSeries -*) +include "transc/TaylorSeries.ma". (* UNEXPORTED Opaque Min Max. @@ -35,20 +35,20 @@ The main properties of the exponential and logarithmic functions. Exponential is strongly extensional and well defined. *) -inline cic:/CoRN/transc/Exponential/Exp_strext.con. +inline "cic:/CoRN/transc/Exponential/Exp_strext.con". -inline cic:/CoRN/transc/Exponential/Exp_wd.con. +inline "cic:/CoRN/transc/Exponential/Exp_wd.con". (* UNEXPORTED Hint Resolve Exp_wd: algebra. *) -inline cic:/CoRN/transc/Exponential/Exp_zero.con. +inline "cic:/CoRN/transc/Exponential/Exp_zero.con". (*#* $e^1=e$#e1=e#, where [e] was defined a long time ago. *) -inline cic:/CoRN/transc/Exponential/Exp_one.con. +inline "cic:/CoRN/transc/Exponential/Exp_one.con". (* UNEXPORTED Hint Resolve Exp_zero Exp_one: algebra. @@ -58,13 +58,13 @@ Hint Resolve Exp_zero Exp_one: algebra. The exponential function is its own derivative, and continuous. *) -inline cic:/CoRN/transc/Exponential/Derivative_Exp.con. +inline "cic:/CoRN/transc/Exponential/Derivative_Exp.con". (* UNEXPORTED Hint Resolve Derivative_Exp: derivate. *) -inline cic:/CoRN/transc/Exponential/Continuous_Exp.con. +inline "cic:/CoRN/transc/Exponential/Continuous_Exp.con". (* UNEXPORTED Hint Resolve Continuous_Exp: continuous. @@ -74,20 +74,20 @@ Hint Resolve Continuous_Exp: continuous. Negative numbers are projected into the interval [[0,1]]. *) -inline cic:/CoRN/transc/Exponential/One_less_Exp.con. +inline "cic:/CoRN/transc/Exponential/One_less_Exp.con". -inline cic:/CoRN/transc/Exponential/One_leEq_Exp.con. +inline "cic:/CoRN/transc/Exponential/One_leEq_Exp.con". -inline cic:/CoRN/transc/Exponential/Exp_pos'.con. +inline "cic:/CoRN/transc/Exponential/Exp_pos'.con". (*#* Exponential is the unique function which evaluates to 1 at 0 and is its own derivative. *) -inline cic:/CoRN/transc/Exponential/Exp_unique_lemma.con. +inline "cic:/CoRN/transc/Exponential/Exp_unique_lemma.con". -inline cic:/CoRN/transc/Exponential/Exp_bnd.con. +inline "cic:/CoRN/transc/Exponential/Exp_bnd.con". (* UNEXPORTED Opaque Expon. @@ -97,25 +97,25 @@ Opaque Expon. Transparent Expon. *) -inline cic:/CoRN/transc/Exponential/Exp_unique.con. +inline "cic:/CoRN/transc/Exponential/Exp_unique.con". (* UNEXPORTED Opaque Expon. *) -inline cic:/CoRN/transc/Exponential/Exp_plus_pos.con. +inline "cic:/CoRN/transc/Exponential/Exp_plus_pos.con". (*#* The usual rules for computing the exponential of a sum. *) -inline cic:/CoRN/transc/Exponential/Exp_plus.con. +inline "cic:/CoRN/transc/Exponential/Exp_plus.con". (* UNEXPORTED Hint Resolve Exp_plus: algebra. *) -inline cic:/CoRN/transc/Exponential/Exp_plus'.con. +inline "cic:/CoRN/transc/Exponential/Exp_plus'.con". -inline cic:/CoRN/transc/Exponential/Exp_inv_char.con. +inline "cic:/CoRN/transc/Exponential/Exp_inv_char.con". (* UNEXPORTED Hint Resolve Exp_inv_char: algebra. @@ -125,52 +125,52 @@ Hint Resolve Exp_inv_char: algebra. from zero. *) -inline cic:/CoRN/transc/Exponential/Exp_pos.con. +inline "cic:/CoRN/transc/Exponential/Exp_pos.con". -inline cic:/CoRN/transc/Exponential/Exp_ap_zero.con. +inline "cic:/CoRN/transc/Exponential/Exp_ap_zero.con". (*#* And the rules for the exponential of differences. *) -inline cic:/CoRN/transc/Exponential/Exp_inv.con. +inline "cic:/CoRN/transc/Exponential/Exp_inv.con". (* UNEXPORTED Hint Resolve Exp_inv: algebra. *) -inline cic:/CoRN/transc/Exponential/Exp_minus.con. +inline "cic:/CoRN/transc/Exponential/Exp_minus.con". (* UNEXPORTED Hint Resolve Exp_minus: algebra. *) -inline cic:/CoRN/transc/Exponential/Exp_inv'.con. +inline "cic:/CoRN/transc/Exponential/Exp_inv'.con". -inline cic:/CoRN/transc/Exponential/Exp_minus'.con. +inline "cic:/CoRN/transc/Exponential/Exp_minus'.con". (*#* Exponential is a monotonous function. *) -inline cic:/CoRN/transc/Exponential/Exp_less_One.con. +inline "cic:/CoRN/transc/Exponential/Exp_less_One.con". -inline cic:/CoRN/transc/Exponential/Exp_leEq_One.con. +inline "cic:/CoRN/transc/Exponential/Exp_leEq_One.con". -inline cic:/CoRN/transc/Exponential/Exp_resp_less.con. +inline "cic:/CoRN/transc/Exponential/Exp_resp_less.con". -inline cic:/CoRN/transc/Exponential/Exp_resp_leEq.con. +inline "cic:/CoRN/transc/Exponential/Exp_resp_leEq.con". (*#* **Properties of Logarithm The logarithm is a continuous function with derivative [One[/]x]. *) -inline cic:/CoRN/transc/Exponential/Derivative_Log.con. +inline "cic:/CoRN/transc/Exponential/Derivative_Log.con". (* UNEXPORTED Hint Resolve Derivative_Log: derivate. *) -inline cic:/CoRN/transc/Exponential/Continuous_Log.con. +inline "cic:/CoRN/transc/Exponential/Continuous_Log.con". (* UNEXPORTED Hint Resolve Continuous_Log: continuous. @@ -178,7 +178,7 @@ Hint Resolve Continuous_Log: continuous. (*#* Logarithm of [One]. *) -inline cic:/CoRN/transc/Exponential/Log_one.con. +inline "cic:/CoRN/transc/Exponential/Log_one.con". (* UNEXPORTED Hint Resolve Log_one: algebra. @@ -186,9 +186,9 @@ Hint Resolve Log_one: algebra. (*#* The logarithm is (strongly) extensional. *) -inline cic:/CoRN/transc/Exponential/Log_strext.con. +inline "cic:/CoRN/transc/Exponential/Log_strext.con". -inline cic:/CoRN/transc/Exponential/Log_wd.con. +inline "cic:/CoRN/transc/Exponential/Log_wd.con". (* UNEXPORTED Hint Resolve Log_wd: algebra. @@ -204,17 +204,17 @@ Opaque Logarithm. Transparent Logarithm. *) -inline cic:/CoRN/transc/Exponential/Log_mult.con. +inline "cic:/CoRN/transc/Exponential/Log_mult.con". (* UNEXPORTED Hint Resolve Log_mult: algebra. *) -inline cic:/CoRN/transc/Exponential/Log_mult'.con. +inline "cic:/CoRN/transc/Exponential/Log_mult'.con". (*#* A characterization of the domain of the logarithm. *) -inline cic:/CoRN/transc/Exponential/Log_domain.con. +inline "cic:/CoRN/transc/Exponential/Log_domain.con". (* UNEXPORTED Opaque Expon Logarithm. @@ -224,9 +224,9 @@ Opaque Expon Logarithm. numerical and as a functional equation. *) -inline cic:/CoRN/transc/Exponential/Log_Exp_inv.con. +inline "cic:/CoRN/transc/Exponential/Log_Exp_inv.con". -inline cic:/CoRN/transc/Exponential/Log_Exp.con. +inline "cic:/CoRN/transc/Exponential/Log_Exp.con". (* UNEXPORTED Transparent Logarithm. @@ -236,11 +236,11 @@ Transparent Logarithm. Hint Resolve Log_Exp: algebra. *) -inline cic:/CoRN/transc/Exponential/Exp_Log_lemma.con. +inline "cic:/CoRN/transc/Exponential/Exp_Log_lemma.con". (*#* The converse expression. *) -inline cic:/CoRN/transc/Exponential/Exp_Log.con. +inline "cic:/CoRN/transc/Exponential/Exp_Log.con". (* UNEXPORTED Hint Resolve Exp_Log: algebra. @@ -248,9 +248,9 @@ Hint Resolve Exp_Log: algebra. (*#* Exponential and logarithm are injective. *) -inline cic:/CoRN/transc/Exponential/Exp_cancel.con. +inline "cic:/CoRN/transc/Exponential/Exp_cancel.con". -inline cic:/CoRN/transc/Exponential/Log_cancel.con. +inline "cic:/CoRN/transc/Exponential/Log_cancel.con". (* UNEXPORTED Opaque Logarithm. @@ -258,9 +258,9 @@ Opaque Logarithm. (*#* And the final characterization as inverse functions. *) -inline cic:/CoRN/transc/Exponential/Exp_Log_inv.con. +inline "cic:/CoRN/transc/Exponential/Exp_Log_inv.con". -inline cic:/CoRN/transc/Exponential/Log_E.con. +inline "cic:/CoRN/transc/Exponential/Log_E.con". (* UNEXPORTED Hint Resolve Log_E: algebra. @@ -268,43 +268,43 @@ Hint Resolve Log_E: algebra. (*#* Several rules regarding inequalities. *) -inline cic:/CoRN/transc/Exponential/Log_cancel_less.con. +inline "cic:/CoRN/transc/Exponential/Log_cancel_less.con". -inline cic:/CoRN/transc/Exponential/Log_cancel_leEq.con. +inline "cic:/CoRN/transc/Exponential/Log_cancel_leEq.con". -inline cic:/CoRN/transc/Exponential/Log_resp_less.con. +inline "cic:/CoRN/transc/Exponential/Log_resp_less.con". -inline cic:/CoRN/transc/Exponential/Log_resp_leEq.con. +inline "cic:/CoRN/transc/Exponential/Log_resp_leEq.con". -inline cic:/CoRN/transc/Exponential/Exp_cancel_less.con. +inline "cic:/CoRN/transc/Exponential/Exp_cancel_less.con". -inline cic:/CoRN/transc/Exponential/Exp_cancel_leEq.con. +inline "cic:/CoRN/transc/Exponential/Exp_cancel_leEq.con". -inline cic:/CoRN/transc/Exponential/Log_less_Zero.con. +inline "cic:/CoRN/transc/Exponential/Log_less_Zero.con". -inline cic:/CoRN/transc/Exponential/Log_leEq_Zero.con. +inline "cic:/CoRN/transc/Exponential/Log_leEq_Zero.con". -inline cic:/CoRN/transc/Exponential/Zero_less_Log.con. +inline "cic:/CoRN/transc/Exponential/Zero_less_Log.con". -inline cic:/CoRN/transc/Exponential/Zero_leEq_Log.con. +inline "cic:/CoRN/transc/Exponential/Zero_leEq_Log.con". (*#* Finally, rules for logarithm of quotients. *) -inline cic:/CoRN/transc/Exponential/Log_recip_char.con. +inline "cic:/CoRN/transc/Exponential/Log_recip_char.con". -inline cic:/CoRN/transc/Exponential/Log_recip.con. +inline "cic:/CoRN/transc/Exponential/Log_recip.con". (* UNEXPORTED Hint Resolve Log_recip: algebra. *) -inline cic:/CoRN/transc/Exponential/Log_recip'.con. +inline "cic:/CoRN/transc/Exponential/Log_recip'.con". -inline cic:/CoRN/transc/Exponential/Log_div.con. +inline "cic:/CoRN/transc/Exponential/Log_div.con". (* UNEXPORTED Hint Resolve Log_div: algebra. *) -inline cic:/CoRN/transc/Exponential/Log_div'.con. +inline "cic:/CoRN/transc/Exponential/Log_div'.con".