Def  Dedekind-Infinite(A) == a:A, f:(AA). 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