Nuprl Definition : vr_RAC
vr_RAC == 
A,B:Type. R:A 
B 
. ((x:A. 
y:B. (R x y)) 
(R':A B . (R' <= R 
(x:A. !y:B. R' x y))))
Definitions occuring in Statement :
vr_sub-rel: R1 <= R2,
vr_exists_uni: !x:T. P[x],
prop: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
apply: f a,
function: x:A B[x],
universe: Type
FDL editor aliases :
vr_RAC
vr\_RAC ==
\mforall{}A,B:Type. \mforall{}R:A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}.
((\mforall{}x:A. \mexists{}y:B. (R x y)) {}\mRightarrow{} (\mexists{}R':A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}. (R' <= R \mwedge{} (\mforall{}x:A. \mexists{}!y:B. R' x y))))
Date html generated:
2012_02_20-PM-03_33_10
Last ObjectModification:
2012_02_02-PM-01_55_17
Home
Index