X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Freals%2FNRootIR.ma;h=0f976d765be65e4630453f83dcff9b6a98157cc9;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=3688480985b751afa3fa2d40a7d5f603099ad361;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/NRootIR.ma b/helm/software/matita/contribs/CoRN-Decl/reals/NRootIR.ma index 368848098..0f976d765 100644 --- a/helm/software/matita/contribs/CoRN-Decl/reals/NRootIR.ma +++ b/helm/software/matita/contribs/CoRN-Decl/reals/NRootIR.ma @@ -16,20 +16,20 @@ set "baseuri" "cic:/matita/CoRN-Decl/reals/NRootIR". +include "CoRN.ma". + (* $Id: NRootIR.v,v 1.5 2004/04/23 10:01:05 lcf Exp $ *) (*#* printing NRoot %\ensuremath{\sqrt[n]{\cdot}}% *) (*#* printing sqrt %\ensuremath{\sqrt{\cdot}}% *) -(* INCLUDE -OddPolyRootIR -*) +include "reals/OddPolyRootIR.ma". (*#* * Roots of Real Numbers *) (* UNEXPORTED -Section NRoot. +Section NRoot *) (*#* ** Existence of roots @@ -39,24 +39,24 @@ Section NRoot. %\end{convention}% *) -inline cic:/CoRN/reals/NRootIR/n.var. +alias id "n" = "cic:/CoRN/reals/NRootIR/NRoot/n.var". -inline cic:/CoRN/reals/NRootIR/n_pos.var. +alias id "n_pos" = "cic:/CoRN/reals/NRootIR/NRoot/n_pos.var". -inline cic:/CoRN/reals/NRootIR/c.var. +alias id "c" = "cic:/CoRN/reals/NRootIR/NRoot/c.var". -inline cic:/CoRN/reals/NRootIR/c_nonneg.var. +alias id "c_nonneg" = "cic:/CoRN/reals/NRootIR/NRoot/c_nonneg.var". (* begin hide *) -inline cic:/CoRN/reals/NRootIR/p.con. +inline "cic:/CoRN/reals/NRootIR/NRoot/p.con" "NRoot__". (* end hide *) -inline cic:/CoRN/reals/NRootIR/CnrootIR.con. +inline "cic:/CoRN/reals/NRootIR/CnrootIR.con". (* UNEXPORTED -End NRoot. +End NRoot *) (*#* We define the root of order [n] for any nonnegative real number and @@ -72,48 +72,48 @@ prove its main properties: *) (* UNEXPORTED -Section Nth_Root. +Section Nth_Root *) -inline cic:/CoRN/reals/NRootIR/nroot.con. +inline "cic:/CoRN/reals/NRootIR/nroot.con". -inline cic:/CoRN/reals/NRootIR/NRoot.con. +inline "cic:/CoRN/reals/NRootIR/NRoot.con". -inline cic:/CoRN/reals/NRootIR/NRoot_power.con. +inline "cic:/CoRN/reals/NRootIR/NRoot_power.con". (* UNEXPORTED Hint Resolve NRoot_power: algebra. *) -inline cic:/CoRN/reals/NRootIR/NRoot_nonneg.con. +inline "cic:/CoRN/reals/NRootIR/NRoot_nonneg.con". -inline cic:/CoRN/reals/NRootIR/NRoot_pos.con. +inline "cic:/CoRN/reals/NRootIR/NRoot_pos.con". -inline cic:/CoRN/reals/NRootIR/NRoot_power'.con. +inline "cic:/CoRN/reals/NRootIR/NRoot_power'.con". -inline cic:/CoRN/reals/NRootIR/NRoot_pres_less.con. +inline "cic:/CoRN/reals/NRootIR/NRoot_pres_less.con". -inline cic:/CoRN/reals/NRootIR/NRoot_less_one.con. +inline "cic:/CoRN/reals/NRootIR/NRoot_less_one.con". -inline cic:/CoRN/reals/NRootIR/NRoot_cancel.con. +inline "cic:/CoRN/reals/NRootIR/NRoot_cancel.con". (*#* %\begin{convention}% Let [x,y] be nonnegative real numbers. %\end{convention}% *) -inline cic:/CoRN/reals/NRootIR/x.var. +alias id "x" = "cic:/CoRN/reals/NRootIR/Nth_Root/x.var". -inline cic:/CoRN/reals/NRootIR/y.var. +alias id "y" = "cic:/CoRN/reals/NRootIR/Nth_Root/y.var". -inline cic:/CoRN/reals/NRootIR/Hx.var. +alias id "Hx" = "cic:/CoRN/reals/NRootIR/Nth_Root/Hx.var". -inline cic:/CoRN/reals/NRootIR/Hy.var. +alias id "Hy" = "cic:/CoRN/reals/NRootIR/Nth_Root/Hy.var". -inline cic:/CoRN/reals/NRootIR/NRoot_wd.con. +inline "cic:/CoRN/reals/NRootIR/NRoot_wd.con". -inline cic:/CoRN/reals/NRootIR/NRoot_unique.con. +inline "cic:/CoRN/reals/NRootIR/NRoot_unique.con". (* UNEXPORTED -End Nth_Root. +End Nth_Root *) (* UNEXPORTED @@ -124,56 +124,56 @@ Implicit Arguments NRoot [x n]. Hint Resolve NRoot_power NRoot_power': algebra. *) -inline cic:/CoRN/reals/NRootIR/NRoot_resp_leEq.con. +inline "cic:/CoRN/reals/NRootIR/NRoot_resp_leEq.con". (*#**********************************) (* UNEXPORTED -Section Square_root. +Section Square_root *) (*#**********************************) (*#* ** Square root *) -inline cic:/CoRN/reals/NRootIR/sqrt.con. +inline "cic:/CoRN/reals/NRootIR/sqrt.con". -inline cic:/CoRN/reals/NRootIR/sqrt_sqr.con. +inline "cic:/CoRN/reals/NRootIR/sqrt_sqr.con". (* UNEXPORTED Hint Resolve sqrt_sqr: algebra. *) -inline cic:/CoRN/reals/NRootIR/sqrt_nonneg.con. +inline "cic:/CoRN/reals/NRootIR/sqrt_nonneg.con". -inline cic:/CoRN/reals/NRootIR/sqrt_wd.con. +inline "cic:/CoRN/reals/NRootIR/sqrt_wd.con". (* UNEXPORTED Hint Resolve sqrt_wd: algebra_c. *) -inline cic:/CoRN/reals/NRootIR/sqrt_to_nonneg.con. +inline "cic:/CoRN/reals/NRootIR/sqrt_to_nonneg.con". -inline cic:/CoRN/reals/NRootIR/sqrt_to_nonpos.con. +inline "cic:/CoRN/reals/NRootIR/sqrt_to_nonpos.con". -inline cic:/CoRN/reals/NRootIR/sqrt_mult.con. +inline "cic:/CoRN/reals/NRootIR/sqrt_mult.con". (* UNEXPORTED Hint Resolve sqrt_mult: algebra. *) -inline cic:/CoRN/reals/NRootIR/sqrt_mult_wd.con. +inline "cic:/CoRN/reals/NRootIR/sqrt_mult_wd.con". -inline cic:/CoRN/reals/NRootIR/sqrt_less.con. +inline "cic:/CoRN/reals/NRootIR/sqrt_less.con". -inline cic:/CoRN/reals/NRootIR/sqrt_less'.con. +inline "cic:/CoRN/reals/NRootIR/sqrt_less'.con". -inline cic:/CoRN/reals/NRootIR/sqrt_resp_leEq.con. +inline "cic:/CoRN/reals/NRootIR/sqrt_resp_leEq.con". -inline cic:/CoRN/reals/NRootIR/sqrt_resp_less.con. +inline "cic:/CoRN/reals/NRootIR/sqrt_resp_less.con". (* UNEXPORTED -End Square_root. +End Square_root *) (* UNEXPORTED @@ -185,7 +185,7 @@ Hint Resolve sqrt_sqr sqrt_mult: algebra. *) (* UNEXPORTED -Section Absolute_Props. +Section Absolute_Props *) (*#* ** More on absolute value @@ -194,60 +194,60 @@ With the help of square roots, we can prove some more properties of absolute values in [IR]. *) -inline cic:/CoRN/reals/NRootIR/AbsIR_sqrt_sqr.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_sqrt_sqr.con". (* UNEXPORTED Hint Resolve AbsIR_sqrt_sqr: algebra. *) -inline cic:/CoRN/reals/NRootIR/AbsIR_resp_mult.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_resp_mult.con". -inline cic:/CoRN/reals/NRootIR/AbsIR_mult_pos.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_mult_pos.con". -inline cic:/CoRN/reals/NRootIR/AbsIR_mult_pos'.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_mult_pos'.con". -inline cic:/CoRN/reals/NRootIR/AbsIR_nexp.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_nexp.con". -inline cic:/CoRN/reals/NRootIR/AbsIR_nexp_op.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_nexp_op.con". -inline cic:/CoRN/reals/NRootIR/AbsIR_less_square.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_less_square.con". -inline cic:/CoRN/reals/NRootIR/AbsIR_leEq_square.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_leEq_square.con". -inline cic:/CoRN/reals/NRootIR/AbsIR_division.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_division.con". (*#* Some special cases. *) -inline cic:/CoRN/reals/NRootIR/AbsIR_recip.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_recip.con". -inline cic:/CoRN/reals/NRootIR/AbsIR_div_two.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_div_two.con". (*#* Cauchy-Schwartz for IR and variants on that subject. *) -inline cic:/CoRN/reals/NRootIR/triangle_IR.con. +inline "cic:/CoRN/reals/NRootIR/triangle_IR.con". -inline cic:/CoRN/reals/NRootIR/triangle_SumIR.con. +inline "cic:/CoRN/reals/NRootIR/triangle_SumIR.con". -inline cic:/CoRN/reals/NRootIR/triangle_IR_minus.con. +inline "cic:/CoRN/reals/NRootIR/triangle_IR_minus.con". -inline cic:/CoRN/reals/NRootIR/weird_triangleIR.con. +inline "cic:/CoRN/reals/NRootIR/weird_triangleIR.con". -inline cic:/CoRN/reals/NRootIR/triangle_IR_minus'.con. +inline "cic:/CoRN/reals/NRootIR/triangle_IR_minus'.con". -inline cic:/CoRN/reals/NRootIR/triangle_SumxIR.con. +inline "cic:/CoRN/reals/NRootIR/triangle_SumxIR.con". -inline cic:/CoRN/reals/NRootIR/triangle_Sum2IR.con. +inline "cic:/CoRN/reals/NRootIR/triangle_Sum2IR.con". -inline cic:/CoRN/reals/NRootIR/AbsIR_str_bnd_AbsIR.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_str_bnd_AbsIR.con". -inline cic:/CoRN/reals/NRootIR/AbsIR_bnd_AbsIR.con. +inline "cic:/CoRN/reals/NRootIR/AbsIR_bnd_AbsIR.con". (* UNEXPORTED -End Absolute_Props. +End Absolute_Props *) (* UNEXPORTED -Section Consequences. +Section Consequences *) (*#* **Cauchy sequences @@ -257,13 +257,13 @@ Cauchy sequence that is never zero and whose Limit is not zero is also a Cauchy sequence. *) -inline cic:/CoRN/reals/NRootIR/Cauchy_Lim_recip.con. +inline "cic:/CoRN/reals/NRootIR/Cauchy_Lim_recip.con". -inline cic:/CoRN/reals/NRootIR/Cauchy_recip.con. +inline "cic:/CoRN/reals/NRootIR/Cauchy_recip.con". -inline cic:/CoRN/reals/NRootIR/Lim_recip.con. +inline "cic:/CoRN/reals/NRootIR/Lim_recip.con". (* UNEXPORTED -End Consequences. +End Consequences *)