IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Dedekind-Infinite(A) ==
a:A, f:(A
A). Inj(A; A; f) &
(
x:A. f(x) = a)
is mentioned
In prior sections:
DiscreteMath
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html