Nuprl - DiscreteMath LEMMAs for nsub_discr_range

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

Rank	Theorem	Name
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]
cites the following:
1	Thm* (A Discrete) (e:(AA). x,y:A. (x e y) x = y)	[discrete_vs_bool]
1	Thm* k:, p:{p:(k)\| i:k. p(i) }. (least i:. p(i)) k	[least_wf]
1	Thm* k:, p:{p:(k)\| i:k. p(i) }. p(least i:. p(i))	[least_satisfies]

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