PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
one2one
preserves
fin
1
1
1
1
1
1
1
1
1
1
1
1
1
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)
a1,a2:
n. (f o f1)(a1) = (f o f1)(a2)
a1 = a2
By:
UnivCD
Generated subgoal:
1
11.
a1:
n
12.
a2:
n
13.
(f o f1)(a1) = (f o f1)(a2)
a1 = a2
About:
n
a1 = a2
U
a1,a2:
a1 = a2
