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