PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
surj
is
inj
gen
1
1
1.
A:
Type
2.
B:
Type
3.
f:
A
B
4.
f1:
A
B
5.
g:
B
A
6.
InvFuns(A; B; f1; g)
7.
n:
8.
f:(
n
B). Bij(
n; B; f)
9.
Surj(A; B; f)
Inj(A; B; f)
By:
RWH (LemmaC
Thm*
(
f:(A
B). Bij(A; B; f))
(A ~ B)) 8
Generated subgoal:
1
8.
n ~ B
9.
Surj(A; B; f)
Inj(A; B; f)
About:
n ~ B
Inj(A; B; f)
BBA
f:(nB). Bij(n; B; f) Inj(A; B; f)f:(AB). Bij(A; B; f)) 
(A ~ B))
8n ~ B Inj(A; B; f)
