PrintForm Definitions finite sets Sections AutomataTheory Doc

At: rect enumer 1

1. n:
2. m:

f:(nm(nm)). Bij(nm; (nm); f)

By: Witness z.1of(z)m+2of(z)

Generated subgoals:

13. z: nm
01of(z)m+2of(z)
23. z: nm
1of(z)m+2of(z) < nm
3 Bij(nm; (nm); z.1of(z)m+2of(z))


About:
existsfunctionproductnatural_numbermultiplylambdaaddless_than