Nuprl - DiscreteMath LEMMAs for compose_iter_bijection

DiscreteMath Sections DiscrMathExt Doc

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

Rank	Theorem	Name
3	Thm* Bij(A; A; f) (i:. Bij(A; A; f{i}))	[compose_iter_bijection]
cites the following:
2	Thm* Inj(A; A; f) (i:. Inj(A; A; f{i}))	[compose_iter_injection]
2	Thm* Surj(A; A; f) (i:. Surj(A; A; f{i}))	[compose_iter_surjection]

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

DiscreteMath Sections DiscrMathExt Doc