PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
one
one
preser
fin
1
1
1
1.
T:
Type
2.
S:
Type
3.
n:
4.
f:
n
T
5.
Bij(
n; T; f)
6.
f1:
T
S
7.
g:
S
T
8.
InvFuns(T; S; f1; g)
n:
, f:(
n
S). Bij(
n; S; f)
By:
Analyze 8
Generated subgoal:
1
8.
g o f1 = Id
9.
f1 o g = Id
n:
, f:(
n
S). Bij(
n; S; f)
About: