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
41 cic:/CoRN/ftc/COrdLemmas/Lemmas/F.var
44 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_lt.con" as lemma.
46 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun.con" as definition.
48 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_1.con" as lemma.
50 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_2a.con" as lemma.
52 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_2.con" as lemma.
54 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_3a.con" as lemma.
56 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_3b.con" as lemma.
58 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4a.con" as lemma.
60 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4b.con" as lemma.
62 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4c.con" as lemma.
64 inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4d.con" as lemma.
69 cic:/CoRN/ftc/COrdLemmas/Lemmas/f.var
73 cic:/CoRN/ftc/COrdLemmas/Lemmas/f0.var
77 cic:/CoRN/ftc/COrdLemmas/Lemmas/f_mon.var
81 cic:/CoRN/ftc/COrdLemmas/Lemmas/h.var
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.
94 inline procedural "cic:/CoRN/ftc/COrdLemmas/Sumx_Sum_Sum
96 (* begin hide *).con" as lemma.
102 inline procedural "cic:/CoRN/ftc/COrdLemmas/str_Sumx_Sum_Sum
104 (* begin hide *).con" as lemma.
114 inline procedural "cic:/CoRN/ftc/COrdLemmas/More_Lemmas/f'.con" "More_Lemmas__" as definition.
119 cic:/CoRN/ftc/COrdLemmas/More_Lemmas/F.var
124 inline procedural "cic:/CoRN/ftc/COrdLemmas/str_Sumx_Sum_Sum'
126 (* begin hide *).con" as lemma.