Nuprl Definition : brouwer_prin_for_fun_27_1ax
brouwer_prin_for_fun_27_1ax{i:l}() ==
A:
((f: . 
B: . (A f B))
(T: List
f:
((t:. !y:. (T [t / mklist(y;f)]) > 0)
(B: . ((t:. y:. ((T [t / mklist(y;f)]) = ((B t) + 1))) (A f B))))))
Definitions occuring in Statement :
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],
add: n + m,
natural_number: $n,
equal: s = t,
mklist: mklist(n;f)
FDL editor aliases :
brouwer_prin_for_fun_27_1ax
brouwer_prin_for_fun_27_1ax
brouwer\_prin\_for\_fun\_27\_1ax\{i:l\}() ==
\mforall{}A:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbP{}
((\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mexists{}B:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (A f B))
{}\mRightarrow{} (\mexists{}T:\mBbbN{} List {}\mrightarrow{} \mBbbN{}
\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}
((\mforall{}t:\mBbbN{}. \mexists{}!y:\mBbbN{}. (T [t / mklist(y;f)]) > 0)
\mwedge{} (\mforall{}B:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((\mforall{}t:\mBbbN{}. \mexists{}y:\mBbbN{}. ((T [t / mklist(y;f)]) = ((B t) + 1))) {}\mRightarrow{} (A f B))))))
Date html generated:
2013_03_20-AM-10_37_47
Last ObjectModification:
2013_03_15-PM-06_48_12
Home
Index