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