Nuprl Definition : vr_GRAC
vr_GRAC ==
A,B:Type. P:A 
. R:A B .
((x:A. ((P x) 
(
y:B. (R x y)))) (R':A B . (R' <= R 
(x:A. ((P x) !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_GRAC
vr\_GRAC ==
\mforall{}A,B:Type. \mforall{}P:A {}\mrightarrow{} \mBbbP{}. \mforall{}R:A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}.
((\mforall{}x:A. ((P x) {}\mRightarrow{} (\mexists{}y:B. (R x y))))
{}\mRightarrow{} (\mexists{}R':A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}. (R' <= R \mwedge{} (\mforall{}x:A. ((P x) {}\mRightarrow{} \mexists{}!y:B. R' x y)))))
Date html generated:
2012_02_20-PM-03_34_52
Last ObjectModification:
2012_02_02-PM-01_55_39
Home
Index