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