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
4	Thm* (A Discrete) (k:, f:(k inj A). f k bij {a:A\| i:k. a = f(i) })	[nsub_inj_discr_range_bijtype]
cites the following:
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]

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