PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
finite
decidable
subset
1
1
1
1.
T:
Type
2.
B:
T
Prop
3.
n:
4.
f:(
n
T). Bij(
n; T; f)
5.
t:T. Dec(B(t))
n ~ T
By:
BackThru
Thm*
(
f:(A
B). Bij(A; B; f))
(A ~ B)
Generated subgoals:
None
About:
Prop
f:(nT). Bij(n; T; f)
t:T. Dec(B(t))
n ~ Tf:(AB). Bij(A; B; f)) 
(A ~ B)
