]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/transc/InvTrigonom.mma
Stuff moved from old Matita.
[helm.git] / matita / matita / contribs / procedural / CoRN / transc / InvTrigonom.mma
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 include "CoRN.ma".
18
19 (* $Id: InvTrigonom.v,v 1.9 2004/04/23 10:01:07 lcf Exp $ *)
20
21 include "transc/RealPowers.ma".
22
23 include "transc/TrigMon.ma".
24
25 include "ftc/StrongIVT.ma".
26
27 (*#* printing ArcSin %\ensuremath{\arcsin}% *)
28
29 (*#* printing ArcCos %\ensuremath{\arccos}% *)
30
31 (*#* printing ArcTan %\ensuremath{\arctan}% *)
32
33 (*#* *Inverse Trigonometric Functions
34
35 **Definitions
36
37 We will now define arcsine, arccosine and arctangent as indefinite
38 integrals and prove their main properties.  We begin by proving that
39 the appropriate indefinite integrals can be defined, then prove the
40 main properties of the function.
41
42 Arccosine is defined in terms of arcsine by the relation
43 [ArcCos(x)=Pi[/]Two-ArcSin(x)].
44
45 ***Arcsine
46 *)
47
48 (* UNEXPORTED
49 Opaque Sine Cosine Expon Logarithm.
50 *)
51
52 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_def_lemma.con" as lemma.
53
54 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_def_zero.con" as lemma.
55
56 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin.con" as definition.
57
58 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_domain.con" as lemma.
59
60 inline procedural "cic:/CoRN/transc/InvTrigonom/Continuous_ArcSin.con" as lemma.
61
62 inline procedural "cic:/CoRN/transc/InvTrigonom/Derivative_ArcSin.con" as lemma.
63
64 (* UNEXPORTED
65 Hint Resolve Derivative_ArcSin: derivate.
66 *)
67
68 (* UNEXPORTED
69 Hint Resolve Continuous_ArcSin: continuous.
70 *)
71
72 (*#* ***Arccosine
73 *)
74
75 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcCos.con" as definition.
76
77 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcCos_domain.con" as lemma.
78
79 inline procedural "cic:/CoRN/transc/InvTrigonom/Continuous_ArcCos.con" as lemma.
80
81 inline procedural "cic:/CoRN/transc/InvTrigonom/Derivative_ArcCos.con" as lemma.
82
83 (*#* ***Arctangent
84 *)
85
86 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_def_lemma.con" as lemma.
87
88 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTang.con" as definition.
89
90 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_domain.con" as lemma.
91
92 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan.con" as definition.
93
94 inline procedural "cic:/CoRN/transc/InvTrigonom/Continuous_ArcTan.con" as lemma.
95
96 inline procedural "cic:/CoRN/transc/InvTrigonom/Derivative_ArcTan.con" as lemma.
97
98 (* UNEXPORTED
99 Hint Resolve Derivative_ArcCos Derivative_ArcTan: derivate.
100 *)
101
102 (* UNEXPORTED
103 Hint Resolve Continuous_ArcCos Continuous_ArcTan: continuous.
104 *)
105
106 (* UNEXPORTED
107 Section Inverses
108 *)
109
110 (*#* **Composition properties
111
112 We now prove that this functions are in fact inverses to the corresponding trigonometric functions.
113
114 ***Sine and Arcsine
115 *)
116
117 inline procedural "cic:/CoRN/transc/InvTrigonom/maps_Sin.con" as lemma.
118
119 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_Sin_inv.con" as lemma.
120
121 (* UNEXPORTED
122 Opaque ArcSin.
123 *)
124
125 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_Sin.con" as lemma.
126
127 (* UNEXPORTED
128 Transparent ArcSin.
129 *)
130
131 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_range.con" as lemma.
132
133 (* UNEXPORTED
134 Transparent ArcSin.
135 *)
136
137 inline procedural "cic:/CoRN/transc/InvTrigonom/Sin_ArcSin.con" as lemma.
138
139 inline procedural "cic:/CoRN/transc/InvTrigonom/Sin_ArcSin_inv.con" as lemma.
140
141 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_resp_leEq.con" as lemma.
142
143 (*#* ***Cosine and Arcosine
144 *)
145
146 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcCos_Cos.con" as lemma.
147
148 inline procedural "cic:/CoRN/transc/InvTrigonom/Cos_ArcCos.con" as lemma.
149
150 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcCos_Cos_inv.con" as lemma.
151
152 inline procedural "cic:/CoRN/transc/InvTrigonom/Cos_ArcCos_inv.con" as lemma.
153
154 (* UNEXPORTED
155 Opaque ArcSin.
156 *)
157
158 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcCos_resp_leEq.con" as lemma.
159
160 (*#* ***Tangent and Arctangent
161 *)
162
163 inline procedural "cic:/CoRN/transc/InvTrigonom/maps_Tan.con" as lemma.
164
165 (* UNEXPORTED
166 Opaque Tang.
167 *)
168
169 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_Tan_inv.con" as lemma.
170
171 (* UNEXPORTED
172 Transparent Tang.
173 *)
174
175 (* UNEXPORTED
176 Opaque ArcTang.
177 *)
178
179 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_Tan.con" as lemma.
180
181 (* UNEXPORTED
182 Opaque iprop.
183 *)
184
185 (* UNEXPORTED
186 Transparent iprop.
187 *)
188
189 (* UNEXPORTED
190 Opaque Cos.
191 *)
192
193 inline procedural "cic:/CoRN/transc/InvTrigonom/Tan_ilim.con" as lemma.
194
195 (* UNEXPORTED
196 Opaque Min.
197 *)
198
199 (* UNEXPORTED
200 Transparent Cos.
201 *)
202
203 (* UNEXPORTED
204 Section ArcTan_Range
205 *)
206
207 (* UNEXPORTED
208 cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/x.var
209 *)
210
211 (* begin hide *)
212
213 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min.con" "Inverses__ArcTan_Range__" as definition.
214
215 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max.con" "Inverses__ArcTan_Range__" as definition.
216
217 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min1.con" "Inverses__ArcTan_Range__" as definition.
218
219 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min2.con" "Inverses__ArcTan_Range__" as definition.
220
221 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min3.con" "Inverses__ArcTan_Range__" as definition.
222
223 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min4.con" "Inverses__ArcTan_Range__" as definition.
224
225 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max1.con" "Inverses__ArcTan_Range__" as definition.
226
227 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max2.con" "Inverses__ArcTan_Range__" as definition.
228
229 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max3.con" "Inverses__ArcTan_Range__" as definition.
230
231 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max4.con" "Inverses__ArcTan_Range__" as definition.
232
233 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min5.con" "Inverses__ArcTan_Range__" as definition.
234
235 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min6.con" "Inverses__ArcTan_Range__" as definition.
236
237 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max5.con" "Inverses__ArcTan_Range__" as definition.
238
239 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max6.con" "Inverses__ArcTan_Range__" as definition.
240
241 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a.con" "Inverses__ArcTan_Range__" as definition.
242
243 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a1.con" "Inverses__ArcTan_Range__" as definition.
244
245 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a2.con" "Inverses__ArcTan_Range__" as definition.
246
247 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a3.con" "Inverses__ArcTan_Range__" as definition.
248
249 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a4.con" "Inverses__ArcTan_Range__" as definition.
250
251 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a5.con" "Inverses__ArcTan_Range__" as definition.
252
253 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b.con" "Inverses__ArcTan_Range__" as definition.
254
255 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b1.con" "Inverses__ArcTan_Range__" as definition.
256
257 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b2.con" "Inverses__ArcTan_Range__" as definition.
258
259 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b3.con" "Inverses__ArcTan_Range__" as definition.
260
261 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b4.con" "Inverses__ArcTan_Range__" as definition.
262
263 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b5.con" "Inverses__ArcTan_Range__" as definition.
264
265 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/ab.con" "Inverses__ArcTan_Range__" as definition.
266
267 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_range_lemma.con" as lemma.
268
269 (* end hide *)
270
271 (* UNEXPORTED
272 Transparent ArcTang.
273 *)
274
275 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_range.con" as lemma.
276
277 (* UNEXPORTED
278 End ArcTan_Range
279 *)
280
281 (* UNEXPORTED
282 Transparent ArcTang.
283 *)
284
285 inline procedural "cic:/CoRN/transc/InvTrigonom/Tan_ArcTan.con" as lemma.
286
287 (* UNEXPORTED
288 Opaque ArcTang.
289 *)
290
291 inline procedural "cic:/CoRN/transc/InvTrigonom/Tan_ArcTan_inv.con" as lemma.
292
293 (* UNEXPORTED
294 End Inverses
295 *)
296