]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma
librarySync - we do not generate the object attributes when we publish the xml
[helm.git] / matita / contribs / CoRN-Decl / ftc / CalculusTheorems.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/CalculusTheorems".
18
19 include "CoRN.ma".
20
21 (* $Id: CalculusTheorems.v,v 1.6 2004/04/23 10:00:57 lcf Exp $ *)
22
23 include "ftc/Rolle.ma".
24
25 include "tactics/DiffTactics3.ma".
26
27 (* UNEXPORTED
28 Opaque Min Max.
29 *)
30
31 (* UNEXPORTED
32 Section Various_Theorems
33 *)
34
35 (*#* *Calculus Theorems
36
37 This file is intended to present a collection of miscellaneous, mostly
38 technical results in differential calculus that are interesting or
39 useful in future work.
40
41 We begin with some properties of continuous functions.  Every
42 continuous function commutes with the limit of a numerical sequence
43 (sometimes called Heine continuity).
44 *)
45
46 inline "cic:/CoRN/ftc/CalculusTheorems/Continuous_imp_comm_Lim.con".
47
48 (*#*
49 This is a tricky result: if [F] is continuous and positive in both [[a,b]]
50 and [(b,c]], then it is positive in [[a,c]].
51 *)
52
53 inline "cic:/CoRN/ftc/CalculusTheorems/Continuous_imp_pos.con".
54
55 (*#*
56 Similar results for increasing functions:
57 *)
58
59 inline "cic:/CoRN/ftc/CalculusTheorems/strict_inc_glues.con".
60
61 inline "cic:/CoRN/ftc/CalculusTheorems/strict_inc_glues'.con".
62
63 inline "cic:/CoRN/ftc/CalculusTheorems/strict_dec_glues.con".
64
65 inline "cic:/CoRN/ftc/CalculusTheorems/strict_dec_glues'.con".
66
67 (*#* More on glueing intervals. *)
68
69 inline "cic:/CoRN/ftc/CalculusTheorems/olor_pos_clor_nonneg.con".
70
71 inline "cic:/CoRN/ftc/CalculusTheorems/olor_pos_olcr_nonneg.con".
72
73 inline "cic:/CoRN/ftc/CalculusTheorems/olor_pos_clcr_nonneg.con".
74
75 (*#*
76 Any function that has the null function as its derivative must be constant.
77 *)
78
79 inline "cic:/CoRN/ftc/CalculusTheorems/FConst_prop.con".
80
81 (*#* As a corollary, two functions with the same derivative must differ
82 by a constant.
83 *)
84
85 inline "cic:/CoRN/ftc/CalculusTheorems/Feq_crit_with_const.con".
86
87 (*#* This yields the following known result: any differential equation
88 of the form [f'=g] with initial condition [f(a) [=] b] has a unique solution.
89 *)
90
91 inline "cic:/CoRN/ftc/CalculusTheorems/Feq_criterium.con".
92
93 (*#*
94 Finally, a well known result: any function with a (strictly) positive
95 derivative is (strictly) increasing.  Although the two lemmas look
96 quite similar the proofs are completely different, both from the
97 formalization and from the mathematical point of view.
98 *)
99
100 inline "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_less.con".
101
102 inline "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_leEq.con".
103
104 inline "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_less'.con".
105
106 (*#* From these results we can finally prove that exponentiation to a
107 real power preserves the less or equal than relation!
108 *)
109
110 (* UNEXPORTED
111 Opaque nring.
112 *)
113
114 (* UNEXPORTED
115 Transparent nring.
116 *)
117
118 inline "cic:/CoRN/ftc/CalculusTheorems/nexp_resp_leEq_odd.con".
119
120 (* UNEXPORTED
121 End Various_Theorems
122 *)
123