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 include "CoRN.ma".
  20
  21 (* begin hide *)
  22
  23 include "reals/Q_in_CReals.ma".
  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 alias id "OF" = "cic:/CoRN/reals/Q_dense/Interval_definition/OF.var".
  34
  35 inline "cic:/CoRN/reals/Q_dense/Interval.ind".
  36
  37 coercion cic:/matita/CoRN-Decl/reals/Q_dense/pair_crr.con 0 (* compounds *).
  38
  39 inline "cic:/CoRN/reals/Q_dense/Length.con".
  40
  41 (* UNEXPORTED
  42 End Interval_definition
  43 *)
  44
  45 inline "cic:/CoRN/reals/Q_dense/Rat_Interval.con".
  46
  47 (* we have this in Q_COrdField... *)
  48
  49 inline "cic:/CoRN/reals/Q_dense/Qlt_eq_gt_dec'.con".
  50
  51 (*
  52 Lemma ex_informative_on_Q:(P:Q_as_COrdField->Prop)(Ex [q:Q_as_COrdField](P q))
  53                              ->{q:Q_as_COrdField | (P q)}.
  54 Proof.
  55  Intro.
  56  Intro.
  57  Apply ex_informative.
  58  Assumption.
  59 Qed.
  60 *)
  61
  62 (* UNEXPORTED
  63 Section COrdField_extra
  64 *)
  65
  66 alias id "OF" = "cic:/CoRN/reals/Q_dense/COrdField_extra/OF.var".
  67
  68 inline "cic:/CoRN/reals/Q_dense/AbsSmall_pos_reflexive.con".
  69
  70 inline "cic:/CoRN/reals/Q_dense/AbsSmall_neg_reflexive.con".
  71
  72 inline "cic:/CoRN/reals/Q_dense/AbsSmall_subinterval.con".
  73
  74 (* UNEXPORTED
  75 End COrdField_extra
  76 *)
  77
  78 (* UNEXPORTED
  79 Section Rational_sequence
  80 *)
  81
  82 include "tactics/Opaque_algebra.ma".
  83
  84 (*#*** WARNING: A file is being loaded *****)
  85
  86 alias id "R1" = "cic:/CoRN/reals/Q_dense/Rational_sequence/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 (* NOTATION
 113 Notation "( A , B )" := (pairT A B).
 114 *)
 115
 116 inline "cic:/CoRN/reals/Q_dense/if_cotrans.con".
 117
 118 inline "cic:/CoRN/reals/Q_dense/if_cotrans_strong.con".
 119
 120 inline "cic:/CoRN/reals/Q_dense/Intrvl.con".
 121
 122 inline "cic:/CoRN/reals/Q_dense/G.con".
 123
 124 (* UNEXPORTED
 125 Opaque Q_as_CField.
 126 *)
 127
 128 inline "cic:/CoRN/reals/Q_dense/delta_Intrvl.con".
 129
 130 inline "cic:/CoRN/reals/Q_dense/Length_Intrvl.con".
 131
 132 inline "cic:/CoRN/reals/Q_dense/Intrvl_inside_l_n.con".
 133
 134 inline "cic:/CoRN/reals/Q_dense/Intrvl_inside_r_n.con".
 135
 136 inline "cic:/CoRN/reals/Q_dense/G_m_n_lower.con".
 137
 138 inline "cic:/CoRN/reals/Q_dense/G_m_n_upper.con".
 139
 140 (* UNEXPORTED
 141 Opaque Q_as_COrdField.
 142 *)
 143
 144 inline "cic:/CoRN/reals/Q_dense/a_simple_inequality.con".
 145
 146 inline "cic:/CoRN/reals/Q_dense/G_conversion_rate2.con".
 147
 148 inline "cic:/CoRN/reals/Q_dense/CS_seq_G.con".
 149
 150 inline "cic:/CoRN/reals/Q_dense/G_as_CauchySeq.con".
 151
 152 inline "cic:/CoRN/reals/Q_dense/CS_seq_inj_Q_G.con".
 153
 154 inline "cic:/CoRN/reals/Q_dense/inj_Q_G_as_CauchySeq.con".
 155
 156 inline "cic:/CoRN/reals/Q_dense/x_in_Intrvl_l.con".
 157
 158 inline "cic:/CoRN/reals/Q_dense/x_in_Intrvl_r.con".
 159
 160 inline "cic:/CoRN/reals/Q_dense/G_conversion_rate_resp_x.con".
 161
 162 inline "cic:/CoRN/reals/Q_dense/x_is_SeqLimit_G.con".
 163
 164 (* UNEXPORTED
 165 End Rational_sequence
 166 *)
 167
 168 (* end hide *)
 169