matita/contribs/CoRN-Decl/transc/TrigMon.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/TrigMon".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: TrigMon.v,v 1.9 2004/04/23 10:01:08 lcf Exp $ *)
  22
  23 include "transc/Pi.ma".
  24
  25 (* UNEXPORTED
  26 Opaque Sine Cosine.
  27 *)
  28
  29 (*#*
  30 Sign properties: cosine is positive in
  31 $(-\frac{\pi}2,\frac{\pi}2)$#(-&pi;/2,&pi;/2)#, sine in
  32 $(0,\pi)$#(0,&pi;)# and tangent in $(0,\frac{\pi}2)$#0,&pi;/2)#.
  33 *)
  34
  35 inline "cic:/CoRN/transc/TrigMon/Cos_pos.con".
  36
  37 inline "cic:/CoRN/transc/TrigMon/Sin_pos.con".
  38
  39 inline "cic:/CoRN/transc/TrigMon/Tan_pos.con".
  40
  41 inline "cic:/CoRN/transc/TrigMon/Cos_nonneg.con".
  42
  43 inline "cic:/CoRN/transc/TrigMon/Sin_nonneg.con".
  44
  45 (*#* Consequences. *)
  46
  47 inline "cic:/CoRN/transc/TrigMon/Abs_Sin_less_One.con".
  48
  49 inline "cic:/CoRN/transc/TrigMon/Abs_Cos_less_One.con".
  50
  51 (*#*
  52 Sine is (strictly) increasing in [[ [--]Pi[/]Two,Pi[/]Two]]; cosine
  53 is (strictly) decreasing in [[Zero,Pi]].
  54 *)
  55
  56 inline "cic:/CoRN/transc/TrigMon/Sin_resp_leEq.con".
  57
  58 inline "cic:/CoRN/transc/TrigMon/Cos_resp_leEq.con".
  59
  60 (* begin hide *)
  61
  62 inline "cic:/CoRN/transc/TrigMon/Cos_resp_less_aux.con".
  63
  64 inline "cic:/CoRN/transc/TrigMon/Cos_resp_less_aux'.con".
  65
  66 (* end hide *)
  67
  68 inline "cic:/CoRN/transc/TrigMon/Cos_resp_less.con".
  69
  70 inline "cic:/CoRN/transc/TrigMon/Sin_resp_less.con".
  71
  72 (* UNEXPORTED
  73 Section Tangent
  74 *)
  75
  76 (*#* **Derivative of Tangent
  77
  78 Finally, two formulas for the derivative of the tangent function and
  79 monotonicity properties.
  80 *)
  81
  82 inline "cic:/CoRN/transc/TrigMon/bnd_Cos.con".
  83
  84 (* UNEXPORTED
  85 Opaque Sine Cosine.
  86 *)
  87
  88 inline "cic:/CoRN/transc/TrigMon/Derivative_Tan_1.con".
  89
  90 inline "cic:/CoRN/transc/TrigMon/Derivative_Tan_2.con".
  91
  92 inline "cic:/CoRN/transc/TrigMon/Tan_resp_less.con".
  93
  94 inline "cic:/CoRN/transc/TrigMon/Tan_resp_leEq.con".
  95
  96 (* UNEXPORTED
  97 End Tangent
  98 *)
  99
 100 (* UNEXPORTED
 101 Hint Resolve Derivative_Tan_1 Derivative_Tan_2: derivate.
 102 *)
 103