]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma
librarySync - we do not generate the object attributes when we publish the xml
[helm.git] / 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