]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/CoRN-Decl/ftc/Derivative.ma
Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals
[helm.git] / matitaB / matita / contribs / CoRN-Decl / ftc / Derivative.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/Derivative".
18
19 include "CoRN.ma".
20
21 (* $Id: Derivative.v,v 1.7 2004/04/23 10:00:58 lcf Exp $ *)
22
23 include "ftc/Continuity.ma".
24
25 (* UNEXPORTED
26 Section Definitions
27 *)
28
29 (*#* *Derivatives
30
31 We will now proceed toward the development of differential calculus.
32 To begin with, the main notion is that of derivative.
33
34 At this stage we will not define a notion of differentiable function,
35 mainly because the natural definition (that of being a function which
36 has some derivative) poses some technical problems; thus, we will
37 postpone that part of our work to a subsequent stage.
38
39 Derivative is a binary relation in the type of partial functions,
40 dependent (once again) on a compact interval with distinct
41 endpoints#. #%\footnote{%As before, we do not define pointwise
42 differentiability, mainly for coherence reasons.  See Bishop [1967]
43 for a discussion on the relative little interest of that concept.%}.%
44 The reason for requiring the endpoints to be apart is mainly to be
45 able to derive the usual properties of the derivative
46 relation---namely, that any two derivatives of the same function must
47 coincide.
48
49 %\begin{convention}% Let [a,b:IR] with [a [<] b] and denote by [I] the
50 interval [[a,b]].  Throughout this chapter, [F, F', G, G'] and [H]
51 will be partial functions with domains respectively [P, P', Q, Q'] and
52 [R].
53 %\end{convention}%
54 *)
55
56 alias id "a" = "cic:/CoRN/ftc/Derivative/Definitions/a.var".
57
58 alias id "b" = "cic:/CoRN/ftc/Derivative/Definitions/b.var".
59
60 alias id "Hab'" = "cic:/CoRN/ftc/Derivative/Definitions/Hab'.var".
61
62 (* begin hide *)
63
64 inline "cic:/CoRN/ftc/Derivative/Definitions/Hab.con" "Definitions__".
65
66 inline "cic:/CoRN/ftc/Derivative/Definitions/I.con" "Definitions__".
67
68 (* end hide *)
69
70 alias id "F" = "cic:/CoRN/ftc/Derivative/Definitions/F.var".
71
72 (* begin hide *)
73
74 inline "cic:/CoRN/ftc/Derivative/Definitions/P.con" "Definitions__".
75
76 (* end hide *)
77
78 inline "cic:/CoRN/ftc/Derivative/Derivative_I.con".
79
80 (* UNEXPORTED
81 End Definitions
82 *)
83
84 (* UNEXPORTED
85 Implicit Arguments Derivative_I [a b].
86 *)
87
88 (* UNEXPORTED
89 Section Basic_Properties
90 *)
91
92 (*#* **Basic Properties
93 *)
94
95 alias id "a" = "cic:/CoRN/ftc/Derivative/Basic_Properties/a.var".
96
97 alias id "b" = "cic:/CoRN/ftc/Derivative/Basic_Properties/b.var".
98
99 alias id "Hab'" = "cic:/CoRN/ftc/Derivative/Basic_Properties/Hab'.var".
100
101 (* begin hide *)
102
103 inline "cic:/CoRN/ftc/Derivative/Basic_Properties/Hab.con" "Basic_Properties__".
104
105 inline "cic:/CoRN/ftc/Derivative/Basic_Properties/I.con" "Basic_Properties__".
106
107 (* end hide *)
108
109 (*#*
110 Like we did for equality, we begin by stating a lemma that makes proofs of derivation easier in practice.
111 *)
112
113 inline "cic:/CoRN/ftc/Derivative/Derivative_I_char.con".
114
115 (* end hide *)
116
117 (*#*
118 Derivative is a well defined relation; we will make this explicit for both arguments:
119 *)
120
121 alias id "F" = "cic:/CoRN/ftc/Derivative/Basic_Properties/F.var".
122
123 alias id "G" = "cic:/CoRN/ftc/Derivative/Basic_Properties/G.var".
124
125 alias id "H" = "cic:/CoRN/ftc/Derivative/Basic_Properties/H.var".
126
127 (* begin hide *)
128
129 inline "cic:/CoRN/ftc/Derivative/Basic_Properties/P.con" "Basic_Properties__".
130
131 inline "cic:/CoRN/ftc/Derivative/Basic_Properties/Q.con" "Basic_Properties__".
132
133 inline "cic:/CoRN/ftc/Derivative/Basic_Properties/R.con" "Basic_Properties__".
134
135 (* end hide *)
136
137 inline "cic:/CoRN/ftc/Derivative/Derivative_I_wdl.con".
138
139 inline "cic:/CoRN/ftc/Derivative/Derivative_I_wdr.con".
140
141 (* begin hide *)
142
143 inline "cic:/CoRN/ftc/Derivative/Basic_Properties/Derivative_I_unique_lemma.con" "Basic_Properties__".
144
145 (* end hide *)
146
147 (*#*
148 Derivative is unique.
149 *)
150
151 inline "cic:/CoRN/ftc/Derivative/Derivative_I_unique.con".
152
153 (*#*
154 Finally, the set where we are considering the relation is included in the domain of both functions.
155 *)
156
157 inline "cic:/CoRN/ftc/Derivative/derivative_imp_inc.con".
158
159 inline "cic:/CoRN/ftc/Derivative/derivative_imp_inc'.con".
160
161 (*#*
162 Any function that is or has a derivative is continuous.
163 *)
164
165 alias id "Hab''" = "cic:/CoRN/ftc/Derivative/Basic_Properties/Hab''.var".
166
167 inline "cic:/CoRN/ftc/Derivative/deriv_imp_contin'_I.con".
168
169 inline "cic:/CoRN/ftc/Derivative/deriv_imp_contin_I.con".
170
171 (* UNEXPORTED
172 End Basic_Properties
173 *)
174
175 (*#*
176 If [G] is the derivative of [F] in a given interval, then [G] is also the derivative of [F] in any smaller interval.
177 *)
178
179 inline "cic:/CoRN/ftc/Derivative/included_imp_deriv.con".
180