matita/contribs/CoRN-Decl/fta/KneserLemma.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/fta/KneserLemma".
  18
  19 (* $Id: KneserLemma.v,v 1.7 2004/04/23 10:00:57 lcf Exp $ *)
  20
  21 (*#* printing Smallest %\ensuremath{\frac13^{2n^2+n}}% *)
  22
  23 (*#* printing eta_0 %\ensuremath{\eta_0}% #&eta;<SUB>0</SUB># *)
  24
  25 (* INCLUDE
  26 NRootCC
  27 *)
  28
  29 (* INCLUDE
  30 AbsCC
  31 *)
  32
  33 (* INCLUDE
  34 MainLemma
  35 *)
  36
  37 (*#* ** Kneser Lemma *)
  38
  39 (* UNEXPORTED
  40 Section Kneser_Lemma.
  41 *)
  42
  43 (*#*
  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
  46 [(AbsCC b_0) [<] c].
  47 %\end{convention}%
  48 *)
  49
  50 inline cic:/CoRN/fta/KneserLemma/b.var.
  51
  52 inline cic:/CoRN/fta/KneserLemma/n.var.
  53
  54 inline cic:/CoRN/fta/KneserLemma/gt_n_0.var.
  55
  56 (* begin hide *)
  57
  58 inline cic:/CoRN/fta/KneserLemma/b_0.con.
  59
  60 inline cic:/CoRN/fta/KneserLemma/b_n.con.
  61
  62 (* end hide *)
  63
  64 inline cic:/CoRN/fta/KneserLemma/b_n_1.var.
  65
  66 inline cic:/CoRN/fta/KneserLemma/c.var.
  67
  68 inline cic:/CoRN/fta/KneserLemma/b_0_lt_c.var.
  69
  70 (*#*
  71 %\begin{convention}% We define the following local abbreviations:
  72  - [two_n := 2 * n]
  73  - [Small := p3m n]
  74  - [Smaller := p3m (two_n * n)]
  75  - [Smallest := Small[*]Smaller]
  76  - [q := One[-]Smallest]
  77  - [a i := AbsCC (b i)]
  78
  79 %\end{convention}%
  80 *)
  81
  82 (* begin hide *)
  83
  84 inline cic:/CoRN/fta/KneserLemma/two_n.con.
  85
  86 inline cic:/CoRN/fta/KneserLemma/Small.con.
  87
  88 inline cic:/CoRN/fta/KneserLemma/Smaller.con.
  89
  90 inline cic:/CoRN/fta/KneserLemma/Smallest.con.
  91
  92 inline cic:/CoRN/fta/KneserLemma/q.con.
  93
  94 (* end hide *)
  95
  96 inline cic:/CoRN/fta/KneserLemma/b_0'_exists.con.
  97
  98 inline cic:/CoRN/fta/KneserLemma/eta_0.con.
  99
 100 inline cic:/CoRN/fta/KneserLemma/eta_0_pos.con.
 101
 102 inline cic:/CoRN/fta/KneserLemma/eta_exists.con.
 103
 104 inline cic:/CoRN/fta/KneserLemma/eps_exists_1.con.
 105
 106 (* less_cotransitive_unfolded on
 107   {Zero  [<]  y[/]x[//]H3[-]Half[*]eps} +
 108   {y[/]x[//]H3[-]Half[*]eps  [<]  Half[*]eps}. *)
 109
 110 inline cic:/CoRN/fta/KneserLemma/eps_exists.con.
 111
 112 (* begin hide *)
 113
 114 inline cic:/CoRN/fta/KneserLemma/a.con.
 115
 116 (* end hide *)
 117
 118 inline cic:/CoRN/fta/KneserLemma/z_exists.con.
 119
 120 (* end hide *)
 121
 122 inline cic:/CoRN/fta/KneserLemma/Kneser_1'.con.
 123
 124 inline cic:/CoRN/fta/KneserLemma/Kneser_1''.con.
 125
 126 inline cic:/CoRN/fta/KneserLemma/Kneser_1.con.
 127
 128 inline cic:/CoRN/fta/KneserLemma/Kneser_2a.con.
 129
 130 inline cic:/CoRN/fta/KneserLemma/Kneser_2b.con.
 131
 132 (* end hide *)
 133
 134 inline cic:/CoRN/fta/KneserLemma/Kneser_2c.con.
 135
 136 (* end hide *)
 137
 138 inline cic:/CoRN/fta/KneserLemma/Kneser_2.con.
 139
 140 (* end hide *)
 141
 142 inline cic:/CoRN/fta/KneserLemma/Kneser_3.con.
 143
 144 (* UNEXPORTED
 145 End Kneser_Lemma.
 146 *)
 147
 148 inline cic:/CoRN/fta/KneserLemma/Kneser.con.
 149