helm/software/matita/contribs/CoRN-Decl/reals/Q_dense.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/reals/Q_dense".
  18
  19 (* begin hide *)
  20
  21 (* INCLUDE
  22 Q_in_CReals
  23 *)
  24
  25 (*#***** Opaque_algebra.v will be loaded in line 151 ******)
  26
  27 inline cic:/CoRN/reals/Q_dense/or_not_and.con.
  28
  29 (* UNEXPORTED
  30 Section Interval_definition.
  31 *)
  32
  33 inline cic:/CoRN/reals/Q_dense/OF.var.
  34
  35 inline cic:/CoRN/reals/Q_dense/Interval.ind.
  36
  37 inline cic:/CoRN/reals/Q_dense/Length.con.
  38
  39 (* UNEXPORTED
  40 End Interval_definition.
  41 *)
  42
  43 inline cic:/CoRN/reals/Q_dense/Rat_Interval.con.
  44
  45 (* we have this in Q_COrdField... *)
  46
  47 inline cic:/CoRN/reals/Q_dense/Qlt_eq_gt_dec'.con.
  48
  49 (*
  50 Lemma ex_informative_on_Q:(P:Q_as_COrdField->Prop)(Ex [q:Q_as_COrdField](P q))
  51                              ->{q:Q_as_COrdField | (P q)}.
  52 Proof.
  53  Intro.
  54  Intro.
  55  Apply ex_informative.
  56  Assumption.
  57 Qed.
  58 *)
  59
  60 (* UNEXPORTED
  61 Section COrdField_extra.
  62 *)
  63
  64 inline cic:/CoRN/reals/Q_dense/OF.var.
  65
  66 inline cic:/CoRN/reals/Q_dense/AbsSmall_pos_reflexive.con.
  67
  68 inline cic:/CoRN/reals/Q_dense/AbsSmall_neg_reflexive.con.
  69
  70 inline cic:/CoRN/reals/Q_dense/AbsSmall_subinterval.con.
  71
  72 (* UNEXPORTED
  73 End COrdField_extra.
  74 *)
  75
  76 (* UNEXPORTED
  77 Section Rational_sequence.
  78 *)
  79
  80 (* INCLUDE
  81 Opaque_algebra
  82 *)
  83
  84 (*#*** WARNING: A file is being loaded *****)
  85
  86 inline cic:/CoRN/reals/Q_dense/R1.var.
  87
  88 inline cic:/CoRN/reals/Q_dense/start_l.con.
  89
  90 inline cic:/CoRN/reals/Q_dense/start_of_sequence2.con.
  91
  92 inline cic:/CoRN/reals/Q_dense/start_r.con.
  93
  94 inline cic:/CoRN/reals/Q_dense/start_of_sequence_property.con.
  95
  96 inline cic:/CoRN/reals/Q_dense/l_less_r.con.
  97
  98 inline cic:/CoRN/reals/Q_dense/shrink23.con.
  99
 100 inline cic:/CoRN/reals/Q_dense/shrink13.con.
 101
 102 inline cic:/CoRN/reals/Q_dense/shrink24.con.
 103
 104 inline cic:/CoRN/reals/Q_dense/cotrans_analyze.con.
 105
 106 inline cic:/CoRN/reals/Q_dense/cotrans_analyze_strong.con.
 107
 108 inline cic:/CoRN/reals/Q_dense/trichotomy.con.
 109
 110 inline cic:/CoRN/reals/Q_dense/trichotomy_strong1.con.
 111
 112 inline cic:/CoRN/reals/Q_dense/if_cotrans.con.
 113
 114 inline cic:/CoRN/reals/Q_dense/if_cotrans_strong.con.
 115
 116 inline cic:/CoRN/reals/Q_dense/Intrvl.con.
 117
 118 inline cic:/CoRN/reals/Q_dense/G.con.
 119
 120 (* UNEXPORTED
 121 Opaque Q_as_CField.
 122 *)
 123
 124 inline cic:/CoRN/reals/Q_dense/delta_Intrvl.con.
 125
 126 inline cic:/CoRN/reals/Q_dense/Length_Intrvl.con.
 127
 128 inline cic:/CoRN/reals/Q_dense/Intrvl_inside_l_n.con.
 129
 130 inline cic:/CoRN/reals/Q_dense/Intrvl_inside_r_n.con.
 131
 132 inline cic:/CoRN/reals/Q_dense/G_m_n_lower.con.
 133
 134 inline cic:/CoRN/reals/Q_dense/G_m_n_upper.con.
 135
 136 (* UNEXPORTED
 137 Opaque Q_as_COrdField.
 138 *)
 139
 140 inline cic:/CoRN/reals/Q_dense/a_simple_inequality.con.
 141
 142 inline cic:/CoRN/reals/Q_dense/G_conversion_rate2.con.
 143
 144 inline cic:/CoRN/reals/Q_dense/CS_seq_G.con.
 145
 146 inline cic:/CoRN/reals/Q_dense/G_as_CauchySeq.con.
 147
 148 inline cic:/CoRN/reals/Q_dense/CS_seq_inj_Q_G.con.
 149
 150 inline cic:/CoRN/reals/Q_dense/inj_Q_G_as_CauchySeq.con.
 151
 152 inline cic:/CoRN/reals/Q_dense/x_in_Intrvl_l.con.
 153
 154 inline cic:/CoRN/reals/Q_dense/x_in_Intrvl_r.con.
 155
 156 inline cic:/CoRN/reals/Q_dense/G_conversion_rate_resp_x.con.
 157
 158 inline cic:/CoRN/reals/Q_dense/x_is_SeqLimit_G.con.
 159
 160 (* UNEXPORTED
 161 End Rational_sequence.
 162 *)
 163
 164 (* end hide *)
 165