Nuprl Definition : vr_RINV
vr_RINV(f;A;B) == 
g:B 
A. 
y:B. (y = (f (g y)))
Definitions occuring in Statement :
all: x:A. B[x],
exists: x:A. B[x],
apply: f a,
function: x:A B[x],
equal: s = t
FDL editor aliases :
vr_RINV
vr\_RINV(f;A;B) == \mexists{}g:B {}\mrightarrow{} A. \mforall{}y:B. (y = (f (g y)))
Date html generated:
2012_02_20-PM-03_34_36
Last ObjectModification:
2012_02_02-PM-01_55_36
Home
Index