Nuprl Definition : vr_AC
vr_AC == 
[A,B:Type]. [G:A 
B 
]. ((x:A. 
y:B. (G x y)) 
(f:A B. x:A. (G x (f x))))
Definitions occuring in Statement :
uall: [x:A]. B[x],
prop: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x],
universe: Type
FDL editor aliases :
vr_AC
vr\_AC == \mforall{}[A,B:Type]. \mforall{}[G:A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}]. ((\mforall{}x:A. \mexists{}y:B. (G x y)) {}\mRightarrow{} (\mexists{}f:A {}\mrightarrow{} B. \mforall{}x:A. (G x (f x))))
Date html generated:
2012_02_20-PM-03_32_51
Last ObjectModification:
2012_02_02-PM-01_55_13
Home
Index