X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FFTC.ma;h=6e373299c3ca4e02b7a0d8c9df9fd4e9a625dde1;hb=62596f4e0a109e43c9df5da20571827c8b905ce4;hp=75d572a5c8b908d47dc0b2f7521a510d25c4f417;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git diff --git a/matita/contribs/CoRN-Decl/ftc/FTC.ma b/matita/contribs/CoRN-Decl/ftc/FTC.ma index 75d572a5c..6e373299c 100644 --- a/matita/contribs/CoRN-Decl/ftc/FTC.ma +++ b/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". +inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/I.var" "Indefinite_Integral__". -inline "cic:/CoRN/ftc/FTC/F.var". +inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/F.var" "Indefinite_Integral__". -inline "cic:/CoRN/ftc/FTC/contF.var". +inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/contF.var" "Indefinite_Integral__". -inline "cic:/CoRN/ftc/FTC/a.var". +inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/a.var" "Indefinite_Integral__". -inline "cic:/CoRN/ftc/FTC/Ha.var". +inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/Ha.var" "Indefinite_Integral__". 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". +inline "cic:/CoRN/ftc/FTC/FTC/J.var" "FTC__". -inline "cic:/CoRN/ftc/FTC/F.var". +inline "cic:/CoRN/ftc/FTC/FTC/F.var" "FTC__". -inline "cic:/CoRN/ftc/FTC/contF.var". +inline "cic:/CoRN/ftc/FTC/FTC/contF.var" "FTC__". -inline "cic:/CoRN/ftc/FTC/x0.var". +inline "cic:/CoRN/ftc/FTC/FTC/x0.var" "FTC__". -inline "cic:/CoRN/ftc/FTC/Hx0.var". +inline "cic:/CoRN/ftc/FTC/FTC/Hx0.var" "FTC__". (* 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". +inline "cic:/CoRN/ftc/FTC/FTC/pJ.var" "FTC__". 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". +inline "cic:/CoRN/ftc/FTC/FTC/G0.var" "FTC__". -inline "cic:/CoRN/ftc/FTC/derG0.var". +inline "cic:/CoRN/ftc/FTC/FTC/derG0.var" "FTC__". 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". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/J.var" "Limit_of_Integral_Seq__". -inline "cic:/CoRN/ftc/FTC/f.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/f.var" "Limit_of_Integral_Seq__". -inline "cic:/CoRN/ftc/FTC/F.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/F.var" "Limit_of_Integral_Seq__". -inline "cic:/CoRN/ftc/FTC/contf.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contf.var" "Limit_of_Integral_Seq__". -inline "cic:/CoRN/ftc/FTC/contF.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contF.var" "Limit_of_Integral_Seq__". (* 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". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/a.var" "Limit_of_Integral_Seq__Compact__". -inline "cic:/CoRN/ftc/FTC/b.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/b.var" "Limit_of_Integral_Seq__Compact__". -inline "cic:/CoRN/ftc/FTC/Hab.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hab.var" "Limit_of_Integral_Seq__Compact__". -inline "cic:/CoRN/ftc/FTC/contIf.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIf.var" "Limit_of_Integral_Seq__Compact__". -inline "cic:/CoRN/ftc/FTC/contIF.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIF.var" "Limit_of_Integral_Seq__Compact__". (* begin show *) -inline "cic:/CoRN/ftc/FTC/convF.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/convF.var" "Limit_of_Integral_Seq__Compact__". (* end show *) -inline "cic:/CoRN/ftc/FTC/x0.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/x0.var" "Limit_of_Integral_Seq__Compact__". -inline "cic:/CoRN/ftc/FTC/Hx0.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0.var" "Limit_of_Integral_Seq__Compact__". -inline "cic:/CoRN/ftc/FTC/Hx0'.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0'.var" "Limit_of_Integral_Seq__Compact__". (* 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". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contg.var" "Limit_of_Integral_Seq__Compact__". -inline "cic:/CoRN/ftc/FTC/contG.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contG.var" "Limit_of_Integral_Seq__Compact__". (* 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". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/convF.var" "Limit_of_Integral_Seq__General__". (* end show *) -inline "cic:/CoRN/ftc/FTC/x0.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/x0.var" "Limit_of_Integral_Seq__General__". -inline "cic:/CoRN/ftc/FTC/Hx0.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/Hx0.var" "Limit_of_Integral_Seq__General__". (* 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". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contg.var" "Limit_of_Integral_Seq__General__". -inline "cic:/CoRN/ftc/FTC/contG.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contG.var" "Limit_of_Integral_Seq__General__". 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". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/J.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/pJ.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/pJ.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/f.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/f.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/g.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/g.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/F.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/F.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/G.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/G.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/contf.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contf.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/contF.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contF.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/convF.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convF.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/contg.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contg.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/contG.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contG.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/convG.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convG.var" "Limit_of_Derivative_Seq__". -inline "cic:/CoRN/ftc/FTC/derf.var". +inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/derf.var" "Limit_of_Derivative_Seq__". 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". +inline "cic:/CoRN/ftc/FTC/Derivative_Series/J.var" "Derivative_Series__". -inline "cic:/CoRN/ftc/FTC/pJ.var". +inline "cic:/CoRN/ftc/FTC/Derivative_Series/pJ.var" "Derivative_Series__". -inline "cic:/CoRN/ftc/FTC/f.var". +inline "cic:/CoRN/ftc/FTC/Derivative_Series/f.var" "Derivative_Series__". -inline "cic:/CoRN/ftc/FTC/g.var". +inline "cic:/CoRN/ftc/FTC/Derivative_Series/g.var" "Derivative_Series__". (* begin show *) -inline "cic:/CoRN/ftc/FTC/convF.var". +inline "cic:/CoRN/ftc/FTC/Derivative_Series/convF.var" "Derivative_Series__". -inline "cic:/CoRN/ftc/FTC/convG.var". +inline "cic:/CoRN/ftc/FTC/Derivative_Series/convG.var" "Derivative_Series__". (* end show *) -inline "cic:/CoRN/ftc/FTC/derF.var". +inline "cic:/CoRN/ftc/FTC/Derivative_Series/derF.var" "Derivative_Series__". inline "cic:/CoRN/ftc/FTC/Derivative_FSeries.con". (* UNEXPORTED -End Derivative_Series. +End Derivative_Series *)