X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FInvTrigonom.ma;h=73a386b025cbdac4eb516739284fc0e5e40b6629;hb=1d8389a897e804825909cc84640e0d5c5f58e543;hp=6ec5b90b431e84595e369da6bfc2f58a7a9a4640;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma b/helm/software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma index 6ec5b90b4..73a386b02 100644 --- a/helm/software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma +++ b/helm/software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma @@ -16,19 +16,15 @@ set "baseuri" "cic:/matita/CoRN-Decl/transc/InvTrigonom". +include "CoRN.ma". + (* $Id: InvTrigonom.v,v 1.9 2004/04/23 10:01:07 lcf Exp $ *) -(* INCLUDE -RealPowers -*) +include "transc/RealPowers.ma". -(* INCLUDE -TrigMon -*) +include "transc/TrigMon.ma". -(* INCLUDE -StrongIVT -*) +include "ftc/StrongIVT.ma". (*#* printing ArcSin %\ensuremath{\arcsin}% *) @@ -55,17 +51,17 @@ Arccosine is defined in terms of arcsine by the relation Opaque Sine Cosine Expon Logarithm. *) -inline cic:/CoRN/transc/InvTrigonom/ArcSin_def_lemma.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcSin_def_lemma.con". -inline cic:/CoRN/transc/InvTrigonom/ArcSin_def_zero.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcSin_def_zero.con". -inline cic:/CoRN/transc/InvTrigonom/ArcSin.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcSin.con". -inline cic:/CoRN/transc/InvTrigonom/ArcSin_domain.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcSin_domain.con". -inline cic:/CoRN/transc/InvTrigonom/Continuous_ArcSin.con. +inline "cic:/CoRN/transc/InvTrigonom/Continuous_ArcSin.con". -inline cic:/CoRN/transc/InvTrigonom/Derivative_ArcSin.con. +inline "cic:/CoRN/transc/InvTrigonom/Derivative_ArcSin.con". (* UNEXPORTED Hint Resolve Derivative_ArcSin: derivate. @@ -78,28 +74,28 @@ Hint Resolve Continuous_ArcSin: continuous. (*#* ***Arccosine *) -inline cic:/CoRN/transc/InvTrigonom/ArcCos.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcCos.con". -inline cic:/CoRN/transc/InvTrigonom/ArcCos_domain.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcCos_domain.con". -inline cic:/CoRN/transc/InvTrigonom/Continuous_ArcCos.con. +inline "cic:/CoRN/transc/InvTrigonom/Continuous_ArcCos.con". -inline cic:/CoRN/transc/InvTrigonom/Derivative_ArcCos.con. +inline "cic:/CoRN/transc/InvTrigonom/Derivative_ArcCos.con". (*#* ***Arctangent *) -inline cic:/CoRN/transc/InvTrigonom/ArcTan_def_lemma.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcTan_def_lemma.con". -inline cic:/CoRN/transc/InvTrigonom/ArcTang.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcTang.con". -inline cic:/CoRN/transc/InvTrigonom/ArcTan_domain.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcTan_domain.con". -inline cic:/CoRN/transc/InvTrigonom/ArcTan.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcTan.con". -inline cic:/CoRN/transc/InvTrigonom/Continuous_ArcTan.con. +inline "cic:/CoRN/transc/InvTrigonom/Continuous_ArcTan.con". -inline cic:/CoRN/transc/InvTrigonom/Derivative_ArcTan.con. +inline "cic:/CoRN/transc/InvTrigonom/Derivative_ArcTan.con". (* UNEXPORTED Hint Resolve Derivative_ArcCos Derivative_ArcTan: derivate. @@ -110,7 +106,7 @@ Hint Resolve Continuous_ArcCos Continuous_ArcTan: continuous. *) (* UNEXPORTED -Section Inverses. +Section Inverses *) (*#* **Composition properties @@ -120,59 +116,59 @@ We now prove that this functions are in fact inverses to the corresponding trigo ***Sine and Arcsine *) -inline cic:/CoRN/transc/InvTrigonom/maps_Sin.con. +inline "cic:/CoRN/transc/InvTrigonom/maps_Sin.con". -inline cic:/CoRN/transc/InvTrigonom/ArcSin_Sin_inv.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcSin_Sin_inv.con". (* UNEXPORTED Opaque ArcSin. *) -inline cic:/CoRN/transc/InvTrigonom/ArcSin_Sin.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcSin_Sin.con". (* UNEXPORTED Transparent ArcSin. *) -inline cic:/CoRN/transc/InvTrigonom/ArcSin_range.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcSin_range.con". (* UNEXPORTED Transparent ArcSin. *) -inline cic:/CoRN/transc/InvTrigonom/Sin_ArcSin.con. +inline "cic:/CoRN/transc/InvTrigonom/Sin_ArcSin.con". -inline cic:/CoRN/transc/InvTrigonom/Sin_ArcSin_inv.con. +inline "cic:/CoRN/transc/InvTrigonom/Sin_ArcSin_inv.con". -inline cic:/CoRN/transc/InvTrigonom/ArcSin_resp_leEq.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcSin_resp_leEq.con". (*#* ***Cosine and Arcosine *) -inline cic:/CoRN/transc/InvTrigonom/ArcCos_Cos.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcCos_Cos.con". -inline cic:/CoRN/transc/InvTrigonom/Cos_ArcCos.con. +inline "cic:/CoRN/transc/InvTrigonom/Cos_ArcCos.con". -inline cic:/CoRN/transc/InvTrigonom/ArcCos_Cos_inv.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcCos_Cos_inv.con". -inline cic:/CoRN/transc/InvTrigonom/Cos_ArcCos_inv.con. +inline "cic:/CoRN/transc/InvTrigonom/Cos_ArcCos_inv.con". (* UNEXPORTED Opaque ArcSin. *) -inline cic:/CoRN/transc/InvTrigonom/ArcCos_resp_leEq.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcCos_resp_leEq.con". (*#* ***Tangent and Arctangent *) -inline cic:/CoRN/transc/InvTrigonom/maps_Tan.con. +inline "cic:/CoRN/transc/InvTrigonom/maps_Tan.con". (* UNEXPORTED Opaque Tang. *) -inline cic:/CoRN/transc/InvTrigonom/ArcTan_Tan_inv.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcTan_Tan_inv.con". (* UNEXPORTED Transparent Tang. @@ -182,7 +178,7 @@ Transparent Tang. Opaque ArcTang. *) -inline cic:/CoRN/transc/InvTrigonom/ArcTan_Tan.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcTan_Tan.con". (* UNEXPORTED Opaque iprop. @@ -196,7 +192,7 @@ Transparent iprop. Opaque Cos. *) -inline cic:/CoRN/transc/InvTrigonom/Tan_ilim.con. +inline "cic:/CoRN/transc/InvTrigonom/Tan_ilim.con". (* UNEXPORTED Opaque Min. @@ -207,68 +203,68 @@ Transparent Cos. *) (* UNEXPORTED -Section ArcTan_Range. +Section ArcTan_Range *) -inline cic:/CoRN/transc/InvTrigonom/x.var. +alias id "x" = "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/x.var". (* begin hide *) -inline cic:/CoRN/transc/InvTrigonom/min.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/max.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/min1.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min1.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/min2.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min2.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/min3.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min3.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/min4.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min4.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/max1.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max1.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/max2.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max2.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/max3.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max3.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/max4.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max4.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/min5.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min5.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/min6.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min6.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/max5.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max5.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/max6.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max6.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/a.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/a1.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a1.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/a2.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a2.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/a3.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a3.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/a4.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a4.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/a5.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a5.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/b.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/b1.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b1.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/b2.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b2.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/b3.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b3.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/b4.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b4.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/b5.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b5.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/ab.con. +inline "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/ab.con" "Inverses__ArcTan_Range__". -inline cic:/CoRN/transc/InvTrigonom/ArcTan_range_lemma.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcTan_range_lemma.con". (* end hide *) @@ -276,25 +272,25 @@ inline cic:/CoRN/transc/InvTrigonom/ArcTan_range_lemma.con. Transparent ArcTang. *) -inline cic:/CoRN/transc/InvTrigonom/ArcTan_range.con. +inline "cic:/CoRN/transc/InvTrigonom/ArcTan_range.con". (* UNEXPORTED -End ArcTan_Range. +End ArcTan_Range *) (* UNEXPORTED Transparent ArcTang. *) -inline cic:/CoRN/transc/InvTrigonom/Tan_ArcTan.con. +inline "cic:/CoRN/transc/InvTrigonom/Tan_ArcTan.con". (* UNEXPORTED Opaque ArcTang. *) -inline cic:/CoRN/transc/InvTrigonom/Tan_ArcTan_inv.con. +inline "cic:/CoRN/transc/InvTrigonom/Tan_ArcTan_inv.con". (* UNEXPORTED -End Inverses. +End Inverses *)