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