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
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.
b:
U
11.
a:
n. f1(a) = g(b)
a:
n. (f o f1)(a) = b
By:
Analyze 11
Generated subgoal:
1
11.
a:
n
12.
f1(a) = g(b)
a:
n. (f o f1)(a) = b
About:
n
a:
U
