helm/software/matita/contribs/CoRN-Decl/fta/CC_Props.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/fta/CC_Props".
  18
  19 (* $Id: CC_Props.v,v 1.3 2004/04/23 10:00:56 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 AbsCC
  23 *)
  24
  25 (*#* * More properties of complex numbers
  26 ** Sequences and limits *)
  27
  28 (* UNEXPORTED
  29 Hint Resolve AbsIR_sqrt_sqr: algebra.
  30 *)
  31
  32 inline cic:/CoRN/fta/CC_Props/absCC_absIR_re.con.
  33
  34 inline cic:/CoRN/fta/CC_Props/absCC_absIR_im.con.
  35
  36 inline cic:/CoRN/fta/CC_Props/seq_re.con.
  37
  38 inline cic:/CoRN/fta/CC_Props/seq_im.con.
  39
  40 inline cic:/CoRN/fta/CC_Props/CC_Cauchy_prop.con.
  41
  42 inline cic:/CoRN/fta/CC_Props/CC_CauchySeq.ind.
  43
  44 inline cic:/CoRN/fta/CC_Props/re_is_Cauchy.con.
  45
  46 inline cic:/CoRN/fta/CC_Props/im_is_Cauchy.con.
  47
  48 inline cic:/CoRN/fta/CC_Props/CC_Cauchy2re.con.
  49
  50 inline cic:/CoRN/fta/CC_Props/CC_Cauchy2im.con.
  51
  52 inline cic:/CoRN/fta/CC_Props/LimCC.con.
  53
  54 inline cic:/CoRN/fta/CC_Props/CC_SeqLimit.con.
  55
  56 inline cic:/CoRN/fta/CC_Props/AbsSmall_sqr.con.
  57
  58 inline cic:/CoRN/fta/CC_Props/AbsSmall_AbsCC.con.
  59
  60 inline cic:/CoRN/fta/CC_Props/LimCC_is_lim.con.
  61
  62 inline cic:/CoRN/fta/CC_Props/CC_SeqLimit_uniq.con.
  63
  64 inline cic:/CoRN/fta/CC_Props/CC_SeqLimit_unq.con.
  65
  66 (*#* ** Continuity for [CC]
  67 *)
  68
  69 (* UNEXPORTED
  70 Section Continuity_for_CC.
  71 *)
  72
  73 (*#*
  74 %\begin{convention}% Let [f : CC->CC].
  75 %\end{convention}%
  76 *)
  77
  78 inline cic:/CoRN/fta/CC_Props/f.var.
  79
  80 (* (CSetoid_un_op CC). *)
  81
  82 inline cic:/CoRN/fta/CC_Props/CCfunLim.con.
  83
  84 inline cic:/CoRN/fta/CC_Props/CCcontinAt.con.
  85
  86 inline cic:/CoRN/fta/CC_Props/CCcontin.con.
  87
  88 inline cic:/CoRN/fta/CC_Props/CCfunLim_SeqLimit.con.
  89
  90 inline cic:/CoRN/fta/CC_Props/f_seq.con.
  91
  92 inline cic:/CoRN/fta/CC_Props/poly_pres_lim.con.
  93
  94 (* UNEXPORTED
  95 End Continuity_for_CC.
  96 *)
  97
  98 inline cic:/CoRN/fta/CC_Props/seq_yields_zero.con.
  99