PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
1
2
1
1
1
1.
n:
2.
m:
3.
0 < m
4.
f:
(
(m-1)
n)
(n
m-1)
5.
Bij(
(m-1)
n;
(n
m-1); f)
6.
n = 0
Bij(
m
n;
(n
m);
z.z(0))
By:
Unfold `biject` 0
THEN
Analyze 0
Generated subgoals:
1
Inj(
m
n;
(n
m);
z.z(0))
2
Surj(
m
n;
(n
m);
z.z(0))
About:
Inj(
m
n; (n
m); 
z.z(0)) Surj(mn; (nm); z.z(0))
(m-1)n)(nm-1)(m-1)n; (nm-1); f) Bij(mn; (nm); z.z(0)) Inj(mn; (nm); z.z(0)) Surj(mn; (nm); z.z(0))
