1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: CalculusTheorems.v,v 1.6 2004/04/23 10:00:57 lcf Exp $ *)
21 include "ftc/Rolle.ma".
23 include "tactics/DiffTactics3.ma".
30 Section Various_Theorems
33 (*#* *Calculus Theorems
35 This file is intended to present a collection of miscellaneous, mostly
36 technical results in differential calculus that are interesting or
37 useful in future work.
39 We begin with some properties of continuous functions. Every
40 continuous function commutes with the limit of a numerical sequence
41 (sometimes called Heine continuity).
44 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Continuous_imp_comm_Lim.con" as lemma.
47 This is a tricky result: if [F] is continuous and positive in both [[a,b]]
48 and [(b,c]], then it is positive in [[a,c]].
51 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Continuous_imp_pos.con" as lemma.
54 Similar results for increasing functions:
57 inline procedural "cic:/CoRN/ftc/CalculusTheorems/strict_inc_glues.con" as lemma.
59 inline procedural "cic:/CoRN/ftc/CalculusTheorems/strict_inc_glues'.con" as lemma.
61 inline procedural "cic:/CoRN/ftc/CalculusTheorems/strict_dec_glues.con" as lemma.
63 inline procedural "cic:/CoRN/ftc/CalculusTheorems/strict_dec_glues'.con" as lemma.
65 (*#* More on glueing intervals. *)
67 inline procedural "cic:/CoRN/ftc/CalculusTheorems/olor_pos_clor_nonneg.con" as lemma.
69 inline procedural "cic:/CoRN/ftc/CalculusTheorems/olor_pos_olcr_nonneg.con" as lemma.
71 inline procedural "cic:/CoRN/ftc/CalculusTheorems/olor_pos_clcr_nonneg.con" as lemma.
74 Any function that has the null function as its derivative must be constant.
77 inline procedural "cic:/CoRN/ftc/CalculusTheorems/FConst_prop.con" as lemma.
79 (*#* As a corollary, two functions with the same derivative must differ
83 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Feq_crit_with_const.con" as lemma.
85 (*#* This yields the following known result: any differential equation
86 of the form [f'=g] with initial condition [f(a) [=] b] has a unique solution.
89 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Feq_criterium.con" as lemma.
92 Finally, a well known result: any function with a (strictly) positive
93 derivative is (strictly) increasing. Although the two lemmas look
94 quite similar the proofs are completely different, both from the
95 formalization and from the mathematical point of view.
98 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_less.con" as lemma.
100 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_leEq.con" as lemma.
102 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_less'.con" as lemma.
104 (*#* From these results we can finally prove that exponentiation to a
105 real power preserves the less or equal than relation!
116 inline procedural "cic:/CoRN/ftc/CalculusTheorems/nexp_resp_leEq_odd.con" as lemma.