1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: COrdLemmas.v,v 1.2 2004/04/23 10:00:57 lcf Exp $ *)
21 include "algebra/COrdCauchy.ma".
27 (*#* *Lemmas for Integration
29 Here we include several lemmas valid in any ordered field [F] which
30 are useful for integration.
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
40 alias id "F" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/F.var".
42 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_lt.con".
44 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun.con".
46 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_1.con".
48 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_2a.con".
50 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_2.con".
52 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_3a.con".
54 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_3b.con".
56 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4a.con".
58 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4b.con".
60 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4c.con".
62 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4d.con".
66 alias id "f" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f.var".
68 alias id "f0" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f0.var".
70 alias id "f_mon" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/f_mon.var".
72 alias id "h" = "cic:/CoRN/ftc/COrdLemmas/Lemmas/h.var".
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.
84 inline procedural "cic:/CoRN/ftc/COrdLemmas/Sumx_Sum_Sum
86 (* begin hide *).con".
92 inline procedural "cic:/CoRN/ftc/COrdLemmas/str_Sumx_Sum_Sum
94 (* begin hide *).con".
104 inline procedural "cic:/CoRN/ftc/COrdLemmas/More_Lemmas/f'.con" "More_Lemmas__".
108 alias id "F" = "cic:/CoRN/ftc/COrdLemmas/More_Lemmas/F.var".
112 inline procedural "cic:/CoRN/ftc/COrdLemmas/str_Sumx_Sum_Sum'
114 (* begin hide *).con".