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