Nuprl Definition : fan_27_7a
fan_27_7a{i:l}() ==
A:
. B: List .
((f: . ((f 
fspr(B)) 
(
b:. (A f b))))
(z:. f: . ((f fspr(B)) (b:. G: . ((G fspr(B)) equal_upto(z;f;G) (A G b))))))
Definitions occuring in Statement :
equal_upto: equal_upto(n;f;g),
in_fin_spr: (f fspr(B)),
nat: ,
prop: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x]
FDL editor aliases :
fan_27_7a
fan\_27\_7a\{i:l\}() ==
\mforall{}A:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbP{}. \mforall{}B:\mBbbN{} List {}\mrightarrow{} \mBbbN{}.
((\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f \mmember{} fspr(B)) {}\mRightarrow{} (\mexists{}b:\mBbbN{}. (A f b))))
{}\mRightarrow{} (\mexists{}z:\mBbbN{}
\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}
((f \mmember{} fspr(B)) {}\mRightarrow{} (\mexists{}b:\mBbbN{}. \mforall{}G:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((G \mmember{} fspr(B)) {}\mRightarrow{} equal\_upto(z;f;G) {}\mRightarrow{} (A G b))))))
Date html generated:
2013_03_20-AM-10_39_06
Last ObjectModification:
2013_03_17-PM-05_52_51
Home
Index