Def  Infinite(A) == ( inj A)

is mentioned by

Thm*  Dedekind-Infinite(A)  Infinite(A)	[dedekind_inf_imp_inf]
Thm*  (A:Type. Finite(A)  Infinite(A))  (D:Type. (D)  (D))	[absurd_nonfinite_imp_infinite]
Thm*  k:. Infinite(k)	[nsub_not_infinite]
Thm*  (A ~ B)  Infinite(A)  Infinite(B)	[ooc_preserves_infiniteness]
Thm*  Infinite(A)  Finite(A)	[infinite_imp_nonfinite]
Thm*  Infinite(A)  Unbounded(A)	[unboundedly_imp_productively_infinite]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html