Nuprl - DiscreteMath LEMMAs for nsub_inj_discr_range

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
3	Thm* (A Discrete) Thm* Thm* (k:, f:(k inj A). Thm* ({a:A\| i:k. a = f(i) } Type Thm* (& f k{a:A\| i:k. a = f(i) } Thm* (& Bij(k; {a:A\| i:k. a = f(i) }; f))	[nsub_inj_discr_range_bij]
cites the following:
2	Thm* (A Discrete) Thm* Thm* (k:, f:(kA). Thm* ({a:A\| i:k. a = f(i) } Type Thm* (& f k{a:A\| i:k. a = f(i) } Thm* (& Surj(k; {a:A\| i:k. a = f(i) }; f))	[nsub_discr_range_surj]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html