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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/fta/KneserLemma".
19 (* $Id: KneserLemma.v,v 1.7 2004/04/23 10:00:57 lcf Exp $ *)
21 (*#* printing Smallest %\ensuremath{\frac13^{2n^2+n}}% *)
23 (*#* printing eta_0 %\ensuremath{\eta_0}% #η<SUB>0</SUB># *)
37 (*#* ** Kneser Lemma *)
44 %\begin{convention}% Let [b : nat->CC], [n : nat] and [c : IR]
45 such that [0 < n], [b_0 := b 0], [b_n := (b n) [=] One] and
50 inline cic:/CoRN/fta/KneserLemma/b.var.
52 inline cic:/CoRN/fta/KneserLemma/n.var.
54 inline cic:/CoRN/fta/KneserLemma/gt_n_0.var.
58 inline cic:/CoRN/fta/KneserLemma/b_0.con.
60 inline cic:/CoRN/fta/KneserLemma/b_n.con.
64 inline cic:/CoRN/fta/KneserLemma/b_n_1.var.
66 inline cic:/CoRN/fta/KneserLemma/c.var.
68 inline cic:/CoRN/fta/KneserLemma/b_0_lt_c.var.
71 %\begin{convention}% We define the following local abbreviations:
74 - [Smaller := p3m (two_n * n)]
75 - [Smallest := Small[*]Smaller]
76 - [q := One[-]Smallest]
77 - [a i := AbsCC (b i)]
84 inline cic:/CoRN/fta/KneserLemma/two_n.con.
86 inline cic:/CoRN/fta/KneserLemma/Small.con.
88 inline cic:/CoRN/fta/KneserLemma/Smaller.con.
90 inline cic:/CoRN/fta/KneserLemma/Smallest.con.
92 inline cic:/CoRN/fta/KneserLemma/q.con.
96 inline cic:/CoRN/fta/KneserLemma/b_0'_exists.con.
98 inline cic:/CoRN/fta/KneserLemma/eta_0.con.
100 inline cic:/CoRN/fta/KneserLemma/eta_0_pos.con.
102 inline cic:/CoRN/fta/KneserLemma/eta_exists.con.
104 inline cic:/CoRN/fta/KneserLemma/eps_exists_1.con.
106 (* less_cotransitive_unfolded on
107 {Zero [<] y[/]x[//]H3[-]Half[*]eps} +
108 {y[/]x[//]H3[-]Half[*]eps [<] Half[*]eps}. *)
110 inline cic:/CoRN/fta/KneserLemma/eps_exists.con.
114 inline cic:/CoRN/fta/KneserLemma/a.con.
118 inline cic:/CoRN/fta/KneserLemma/z_exists.con.
122 inline cic:/CoRN/fta/KneserLemma/Kneser_1'.con.
124 inline cic:/CoRN/fta/KneserLemma/Kneser_1''.con.
126 inline cic:/CoRN/fta/KneserLemma/Kneser_1.con.
128 inline cic:/CoRN/fta/KneserLemma/Kneser_2a.con.
130 inline cic:/CoRN/fta/KneserLemma/Kneser_2b.con.
134 inline cic:/CoRN/fta/KneserLemma/Kneser_2c.con.
138 inline cic:/CoRN/fta/KneserLemma/Kneser_2.con.
142 inline cic:/CoRN/fta/KneserLemma/Kneser_3.con.
148 inline cic:/CoRN/fta/KneserLemma/Kneser.con.