Nuprl Definition : brouwer_prin_for_num_27_2_orig
brouwer_prin_for_num_27_2_orig{i:l}() ==
  A:      
    ((f:  . b:. (A f b))
     (T: List  
         f:  
           y:. (((T mklist(y;f)) > 0)  (x:. (((T mklist(x;f)) > 0)  (y = x)))  (A f (T mklist(y;f)--1)))))
Definitions occuring in Statement : 
monus: (a--b), 
nat: , 
prop: , 
gt: i > j, 
all: x:A. B[x], 
exists: x:A. B[x], 
implies: P  Q, 
and: P  Q, 
apply: f a, 
function: x:A  B[x], 
natural_number: $n, 
equal: s = t, 
mklist: mklist(n;f)
FDL editor aliases : 
brouwer_prin_for_num_27_2_orig
brouwer\_prin\_for\_num\_27\_2\_orig\{i:l\}()  ==
    \mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
        ((\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}b:\mBbbN{}.  (A  f  b))
        {}\mRightarrow{}  (\mexists{}T:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}
                  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
                      \mexists{}y:\mBbbN{}
                        (((T  mklist(y;f))  >  0)
                        \mwedge{}  (\mforall{}x:\mBbbN{}.  (((T  mklist(x;f))  >  0)  {}\mRightarrow{}  (y  =  x)))
                        \mwedge{}  (A  f  (T  mklist(y;f)--1)))))
Date html generated:
2013_03_20-AM-10_38_04
Last ObjectModification:
2013_03_17-PM-07_16_22
Home
Index