mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f)

is mentioned by

Thm* k:, i,j:k. Bij(k; k; (i, j))[flip_bijection]
Thm* k:, f:(kk).
Thm* 0<k
Thm* 
Thm* Bij(k; k; f)
Thm* 
Thm* f(k-1) = k-1  f  (k-1)(k-1) & Bij((k-1); (k-1); f)		[bijection_restriction]

In prior sections: fun 1

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb nat Sections MarkB generic Doc