helm/software/matita/contribs/CoRN-Procedural/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 alias id "F" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/F.var".
  41
  42 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_lt.con".
  43
  44 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun.con".
  45
  46 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_1.con".
  47
  48 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_2a.con".
  49
  50 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_2.con".
  51
  52 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_3a.con".
  53
  54 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_3b.con".
  55
  56 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4a.con".
  57
  58 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4b.con".
  59
  60 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4c.con".
  61
  62 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4d.con".
  63
  64 (* begin hide *)
  65
  66 alias id "f" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f.var".
  67
  68 alias id "f0" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f0.var".
  69
  70 alias id "f_mon" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f_mon.var".
  71
  72 alias id "h" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/h.var".
  73
  74 (* end hide *)
  75
  76 (*#* ** Summations
  77 Also, some technical stuff on sums.  The first lemma relates two
  78 different kinds of sums; the other two ones are variations, where the
  79 structure of the arguments is analyzed in more detail.
  80 *)
  81
  82 (* begin show *)
  83
  84 inline procedural "cic:/CoRN/ftc/COrdLemmas/Sumx_Sum_Sum
  85  (* end show *)
  86  (* begin hide *).con".
  87
  88 (* end hide *)
  89
  90 (* begin show *)
  91
  92 inline procedural "cic:/CoRN/ftc/COrdLemmas/str_Sumx_Sum_Sum
  93  (* end show *)
  94  (* begin hide *).con".
  95
  96 (* UNEXPORTED
  97 End Lemmas
  98 *)
  99
 100 (* UNEXPORTED
 101 Section More_Lemmas
 102 *)
 103
 104 inline procedural "cic:/CoRN/ftc/COrdLemmas/More_Lemmas/f'.con" "More_Lemmas__".
 105
 106 (* end hide *)
 107
 108 alias id "F" = "cic:/CoRN/ftc/COrdLemmas/More_Lemmas/F.var".
 109
 110 (* begin show *)
 111
 112 inline procedural "cic:/CoRN/ftc/COrdLemmas/str_Sumx_Sum_Sum'
 113  (* end show *)
 114  (* begin hide *).con".
 115
 116 (* end hide *)
 117
 118 (* UNEXPORTED
 119 End More_Lemmas
 120 *)
 121