Nuprl Definition : brouwer_prin_for_num_simpl
brouwer_prin_for_num_simpl{i:l}() ==
A:
((f: . 
b:. (A f b))
(T: List (?)
f: . (!y:. 
isl(T mklist(y;f)) 
(y:. ((isl(T mklist(y;f))) (A f outl(T mklist(y;f))))))))
Definitions occuring in Statement :
outl: outl(x),
isl: isl(x),
assert: b,
nat: ,
prop: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
unit: Unit,
apply: f a,
function: x:A B[x],
union: left + right,
mklist: mklist(n;f)
FDL editor aliases :
brouwer_prin_for_num_simpl
brouwer\_prin\_for\_num\_simpl\{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{}. \muparrow{}isl(T mklist(y;f))
\mwedge{} (\mforall{}y:\mBbbN{}. ((\muparrow{}isl(T mklist(y;f))) {}\mRightarrow{} (A f outl(T mklist(y;f))))))))
Date html generated:
2013_03_20-AM-10_38_33
Last ObjectModification:
2013_03_17-PM-05_19_01
Home
Index