PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
one2one
preserves
fin
1
1
1
1
1
1
1
1
1
1
1
1
1
2
1
1
1.
T:
Type
2.
U:
Type
3.
f:
T
U
4.
g:
U
T
5.
g o f = Id
6.
f o g = Id
7.
n:
8.
f1:
n
T
9.
Inj(
n; T; f1)
10.
Surj(
n; T; f1)
11.
b:
U
a:
n. (f o f1)(a) = b
By:
Unfold `surject` 10
Generated subgoal:
1
10.
b:T.
a:
n. f1(a) = b
11.
b:
U
a:
n. (f o f1)(a) = b
About:
b:T. 
a:
n. f1(a) = b
U
