matita/contribs/CoRN-Decl/ftc/COrdLemmas.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/ftc/COrdLemmas".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: COrdLemmas.v,v 1.2 2004/04/23 10:00:57 lcf Exp $ *)
  22
  23 include "algebra/COrdCauchy.ma".
  24
  25 (* UNEXPORTED
  26 Section Lemmas
  27 *)
  28
  29 (*#* *Lemmas for Integration
  30
  31 Here we include several lemmas valid in any ordered field [F] which
  32 are useful for integration.
  33
  34 ** Merging orders
  35
  36 We first prove that any two strictly ordered sets of points which have
  37 an empty intersection can be ordered as one (this will be the core of
  38 the proof that any two partitions with no common point have a common
  39 refinement).
  40 *)
  41
  42 alias id "F" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/F.var".
  43
  44 inline "cic:/CoRN/ftc/COrdLemmas/om_fun_lt.con".
  45
  46 inline "cic:/CoRN/ftc/COrdLemmas/om_fun.con".
  47
  48 inline "cic:/CoRN/ftc/COrdLemmas/om_fun_1.con".
  49
  50 inline "cic:/CoRN/ftc/COrdLemmas/om_fun_2a.con".
  51
  52 inline "cic:/CoRN/ftc/COrdLemmas/om_fun_2.con".
  53
  54 inline "cic:/CoRN/ftc/COrdLemmas/om_fun_3a.con".
  55
  56 inline "cic:/CoRN/ftc/COrdLemmas/om_fun_3b.con".
  57
  58 inline "cic:/CoRN/ftc/COrdLemmas/om_fun_4a.con".
  59
  60 inline "cic:/CoRN/ftc/COrdLemmas/om_fun_4b.con".
  61
  62 inline "cic:/CoRN/ftc/COrdLemmas/om_fun_4c.con".
  63
  64 inline "cic:/CoRN/ftc/COrdLemmas/om_fun_4d.con".
  65
  66 (* begin hide *)
  67
  68 alias id "f" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f.var".
  69
  70 alias id "f0" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f0.var".
  71
  72 alias id "f_mon" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f_mon.var".
  73
  74 alias id "h" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/h.var".
  75
  76 (* end hide *)
  77
  78 (*#* ** Summations
  79 Also, some technical stuff on sums.  The first lemma relates two
  80 different kinds of sums; the other two ones are variations, where the
  81 structure of the arguments is analyzed in more detail.
  82 *)
  83
  84 (* begin show *)
  85
  86 inline "cic:/CoRN/ftc/COrdLemmas/Sumx_Sum_Sum
  87  (* end show *)
  88  (* begin hide *).con".
  89
  90 (* end hide *)
  91
  92 (* begin show *)
  93
  94 inline "cic:/CoRN/ftc/COrdLemmas/str_Sumx_Sum_Sum
  95  (* end show *)
  96  (* begin hide *).con".
  97
  98 (* UNEXPORTED
  99 End Lemmas
 100 *)
 101
 102 (* UNEXPORTED
 103 Section More_Lemmas
 104 *)
 105
 106 inline "cic:/CoRN/ftc/COrdLemmas/More_Lemmas/f'.con" "More_Lemmas__".
 107
 108 (* end hide *)
 109
 110 alias id "F" = "cic:/CoRN/ftc/COrdLemmas/More_Lemmas/F.var".
 111
 112 (* begin show *)
 113
 114 inline "cic:/CoRN/ftc/COrdLemmas/str_Sumx_Sum_Sum'
 115  (* end show *)
 116  (* begin hide *).con".
 117
 118 (* end hide *)
 119
 120 (* UNEXPORTED
 121 End More_Lemmas
 122 *)
 123