X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FFTC.ma;h=481eb2b3b4663b38f20eaa363ad7f563a3bb6c04;hb=8c0ccf03dbefd83818bc3b6849634f422f8ec727;hp=75d572a5c8b908d47dc0b2f7521a510d25c4f417;hpb=80110e17ef1d38d71473e9471ce15beddde663bb;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma index 75d572a5c..481eb2b3b 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma @@ -31,7 +31,7 @@ Opaque Min. *) (* UNEXPORTED -Section Indefinite_Integral. +Section Indefinite_Integral *) (*#* *The Fundamental Theorem of Calculus @@ -51,15 +51,15 @@ and [a] be a point in [I]. %\end{convention}% *) -inline "cic:/CoRN/ftc/FTC/I.var". +alias id "I" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/I.var". -inline "cic:/CoRN/ftc/FTC/F.var". +alias id "F" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/F.var". -inline "cic:/CoRN/ftc/FTC/contF.var". +alias id "contF" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/contF.var". -inline "cic:/CoRN/ftc/FTC/a.var". +alias id "a" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/a.var". -inline "cic:/CoRN/ftc/FTC/Ha.var". +alias id "Ha" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/Ha.var". inline "cic:/CoRN/ftc/FTC/prim_lemma.con". @@ -68,15 +68,19 @@ inline "cic:/CoRN/ftc/FTC/Fprim_strext.con". inline "cic:/CoRN/ftc/FTC/Fprim.con". (* UNEXPORTED -End Indefinite_Integral. +End Indefinite_Integral *) (* UNEXPORTED Implicit Arguments Fprim [I F]. *) +(* NOTATION +Notation "[-S-] F" := (Fprim F) (at level 20). +*) + (* UNEXPORTED -Section FTC. +Section FTC *) (*#* **The FTC @@ -90,19 +94,19 @@ indefinite integral of [F] from [x0]. %\end{convention}% *) -inline "cic:/CoRN/ftc/FTC/J.var". +alias id "J" = "cic:/CoRN/ftc/FTC/FTC/J.var". -inline "cic:/CoRN/ftc/FTC/F.var". +alias id "F" = "cic:/CoRN/ftc/FTC/FTC/F.var". -inline "cic:/CoRN/ftc/FTC/contF.var". +alias id "contF" = "cic:/CoRN/ftc/FTC/FTC/contF.var". -inline "cic:/CoRN/ftc/FTC/x0.var". +alias id "x0" = "cic:/CoRN/ftc/FTC/FTC/x0.var". -inline "cic:/CoRN/ftc/FTC/Hx0.var". +alias id "Hx0" = "cic:/CoRN/ftc/FTC/FTC/Hx0.var". (* begin hide *) -inline "cic:/CoRN/ftc/FTC/G.con". +inline "cic:/CoRN/ftc/FTC/FTC/G.con" "FTC__". (* end hide *) @@ -112,7 +116,7 @@ inline "cic:/CoRN/ftc/FTC/Continuous_prim.con". The derivative of [G] is simply [F]. *) -inline "cic:/CoRN/ftc/FTC/pJ.var". +alias id "pJ" = "cic:/CoRN/ftc/FTC/FTC/pJ.var". inline "cic:/CoRN/ftc/FTC/FTC1.con". @@ -120,9 +124,9 @@ inline "cic:/CoRN/ftc/FTC/FTC1.con". Any other function [G0] with derivative [F] must differ from [G] by a constant. *) -inline "cic:/CoRN/ftc/FTC/G0.var". +alias id "G0" = "cic:/CoRN/ftc/FTC/FTC/G0.var". -inline "cic:/CoRN/ftc/FTC/derG0.var". +alias id "derG0" = "cic:/CoRN/ftc/FTC/FTC/derG0.var". inline "cic:/CoRN/ftc/FTC/FTC2.con". @@ -132,7 +136,7 @@ The following is another statement of the Fundamental Theorem of Calculus, also (* begin hide *) -inline "cic:/CoRN/ftc/FTC/G0_inc.con". +inline "cic:/CoRN/ftc/FTC/FTC/G0_inc.con" "FTC__". (* end hide *) @@ -145,7 +149,7 @@ inline "cic:/CoRN/ftc/FTC/Barrow.con". (* end hide *) (* UNEXPORTED -End FTC. +End FTC *) (* UNEXPORTED @@ -157,7 +161,7 @@ Hint Resolve FTC1: derivate. *) (* UNEXPORTED -Section Limit_of_Integral_Seq. +Section Limit_of_Integral_Seq *) (*#* **Corollaries @@ -176,18 +180,18 @@ then the sequence of their primitives also converges, and the limit commutes with the indefinite integral. *) -inline "cic:/CoRN/ftc/FTC/J.var". +alias id "J" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/J.var". -inline "cic:/CoRN/ftc/FTC/f.var". +alias id "f" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/f.var". -inline "cic:/CoRN/ftc/FTC/F.var". +alias id "F" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/F.var". -inline "cic:/CoRN/ftc/FTC/contf.var". +alias id "contf" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contf.var". -inline "cic:/CoRN/ftc/FTC/contF.var". +alias id "contF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contF.var". (* UNEXPORTED -Section Compact. +Section Compact *) (*#* @@ -200,48 +204,48 @@ continuous in [[a,b]], $x0\in[a,b]$#x0∈[a,b]#; denote by %\end{convention}% *) -inline "cic:/CoRN/ftc/FTC/a.var". +alias id "a" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/a.var". -inline "cic:/CoRN/ftc/FTC/b.var". +alias id "b" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/b.var". -inline "cic:/CoRN/ftc/FTC/Hab.var". +alias id "Hab" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hab.var". -inline "cic:/CoRN/ftc/FTC/contIf.var". +alias id "contIf" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIf.var". -inline "cic:/CoRN/ftc/FTC/contIF.var". +alias id "contIF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIF.var". (* begin show *) -inline "cic:/CoRN/ftc/FTC/convF.var". +alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/convF.var". (* end show *) -inline "cic:/CoRN/ftc/FTC/x0.var". +alias id "x0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/x0.var". -inline "cic:/CoRN/ftc/FTC/Hx0.var". +alias id "Hx0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0.var". -inline "cic:/CoRN/ftc/FTC/Hx0'.var". +alias id "Hx0'" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0'.var". (* begin hide *) -inline "cic:/CoRN/ftc/FTC/g.con". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/g.con" "Limit_of_Integral_Seq__Compact__". -inline "cic:/CoRN/ftc/FTC/G.con". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/G.con" "Limit_of_Integral_Seq__Compact__". (* end hide *) (* begin show *) -inline "cic:/CoRN/ftc/FTC/contg.var". +alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contg.var". -inline "cic:/CoRN/ftc/FTC/contG.var". +alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contG.var". (* end show *) inline "cic:/CoRN/ftc/FTC/fun_lim_seq_integral.con". (* UNEXPORTED -End Compact. +End Compact *) (*#* @@ -253,7 +257,7 @@ inline "cic:/CoRN/ftc/FTC/limit_of_integral.con". inline "cic:/CoRN/ftc/FTC/limit_of_Integral.con". (* UNEXPORTED -Section General. +Section General *) (*#* @@ -262,38 +266,38 @@ Finally, with [x0, g, G] as before, (* begin show *) -inline "cic:/CoRN/ftc/FTC/convF.var". +alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/convF.var". (* end show *) -inline "cic:/CoRN/ftc/FTC/x0.var". +alias id "x0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/x0.var". -inline "cic:/CoRN/ftc/FTC/Hx0.var". +alias id "Hx0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/Hx0.var". (* begin hide *) -inline "cic:/CoRN/ftc/FTC/g.con". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/g.con" "Limit_of_Integral_Seq__General__". -inline "cic:/CoRN/ftc/FTC/G.con". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/G.con" "Limit_of_Integral_Seq__General__". (* end hide *) -inline "cic:/CoRN/ftc/FTC/contg.var". +alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contg.var". -inline "cic:/CoRN/ftc/FTC/contG.var". +alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contG.var". inline "cic:/CoRN/ftc/FTC/fun_lim_seq_integral_IR.con". (* UNEXPORTED -End General. +End General *) (* UNEXPORTED -End Limit_of_Integral_Seq. +End Limit_of_Integral_Seq *) (* UNEXPORTED -Section Limit_of_Derivative_Seq. +Section Limit_of_Derivative_Seq *) (*#* @@ -303,67 +307,67 @@ Similar results hold for the sequence of derivatives of a converging sequence; t %\end{convention}% *) -inline "cic:/CoRN/ftc/FTC/J.var". +alias id "J" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/J.var". -inline "cic:/CoRN/ftc/FTC/pJ.var". +alias id "pJ" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/pJ.var". -inline "cic:/CoRN/ftc/FTC/f.var". +alias id "f" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/f.var". -inline "cic:/CoRN/ftc/FTC/g.var". +alias id "g" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/g.var". -inline "cic:/CoRN/ftc/FTC/F.var". +alias id "F" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/F.var". -inline "cic:/CoRN/ftc/FTC/G.var". +alias id "G" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/G.var". -inline "cic:/CoRN/ftc/FTC/contf.var". +alias id "contf" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contf.var". -inline "cic:/CoRN/ftc/FTC/contF.var". +alias id "contF" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contF.var". -inline "cic:/CoRN/ftc/FTC/convF.var". +alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convF.var". -inline "cic:/CoRN/ftc/FTC/contg.var". +alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contg.var". -inline "cic:/CoRN/ftc/FTC/contG.var". +alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contG.var". -inline "cic:/CoRN/ftc/FTC/convG.var". +alias id "convG" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convG.var". -inline "cic:/CoRN/ftc/FTC/derf.var". +alias id "derf" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/derf.var". inline "cic:/CoRN/ftc/FTC/fun_lim_seq_derivative.con". (* UNEXPORTED -End Limit_of_Derivative_Seq. +End Limit_of_Derivative_Seq *) (* UNEXPORTED -Section Derivative_Series. +Section Derivative_Series *) (*#* As a very important case of this result, we get a rule for deriving series. *) -inline "cic:/CoRN/ftc/FTC/J.var". +alias id "J" = "cic:/CoRN/ftc/FTC/Derivative_Series/J.var". -inline "cic:/CoRN/ftc/FTC/pJ.var". +alias id "pJ" = "cic:/CoRN/ftc/FTC/Derivative_Series/pJ.var". -inline "cic:/CoRN/ftc/FTC/f.var". +alias id "f" = "cic:/CoRN/ftc/FTC/Derivative_Series/f.var". -inline "cic:/CoRN/ftc/FTC/g.var". +alias id "g" = "cic:/CoRN/ftc/FTC/Derivative_Series/g.var". (* begin show *) -inline "cic:/CoRN/ftc/FTC/convF.var". +alias id "convF" = "cic:/CoRN/ftc/FTC/Derivative_Series/convF.var". -inline "cic:/CoRN/ftc/FTC/convG.var". +alias id "convG" = "cic:/CoRN/ftc/FTC/Derivative_Series/convG.var". (* end show *) -inline "cic:/CoRN/ftc/FTC/derF.var". +alias id "derF" = "cic:/CoRN/ftc/FTC/Derivative_Series/derF.var". inline "cic:/CoRN/ftc/FTC/Derivative_FSeries.con". (* UNEXPORTED -End Derivative_Series. +End Derivative_Series *)