Def  Unbounded(A) == k:. (k inj A)

is mentioned by

Thm*  Dedekind-Infinite(A)  Unbounded(A)	[dededing_imp_unb_inf]
Thm*  (A:Type. Finite(A)  Unbounded(A))  (P:Prop. P  P)	[nonfin_eqv_unb_inf_iff_negnegelim]
Thm*  (A:Type. Finite(A)  Unbounded(A))  (D:Type. (D)  (D))	[absurd_nonfin_imp_unb_inf]
Thm*  (P:Prop. P  P)  (A:Type. Finite(A)  Unbounded(A))	[negnegelim_imp_notfin_imp_unb_inf]
Thm*  (A ~ B)  Unbounded(A)  Unbounded(B)	[ooc_preserves_unb_inf]
Thm*  Unbounded(A)  Finite(A)	[unb_inf_not_fin]
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