PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
3
1.
n:
2.
m:
Bij(
n
m;
(n
m);
z.1of(z)
m+2of(z))
By:
Unfold `biject` 0
Generated subgoal:
1
Inj(
n
m;
(n
m);
z.1of(z)
m+2of(z)) & Surj(
n
m;
(n
m);
z.1of(z)
m+2of(z))
About:
Inj(
n
m; (n
m); 
z.1of(z)m+2of(z)) & Surj(nm; (nm); z.1of(z)m+2of(z))
Bij(nm; (nm); z.1of(z)m+2of(z)) Inj(nm; (nm); z.1of(z)m+2of(z)) & Surj(nm; (nm); z.1of(z)m+2of(z))
