helm/software/matita/contribs/procedural/CoRN/reals/Q_dense.mma

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