PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
finite
decidable
subset
1
1.
T:
Type
2.
B:
T
Prop
3.
Fin(T)
4.
t:T. Dec(B(t))
Fin({t:T| B(t) })
By:
Analyze 3
Generated subgoal:
1
3.
n:
4.
f:(
n
T). Bij(
n; T; f)
5.
t:T. Dec(B(t))
Fin({t:T| B(t) })
About:
f:(n
T). Bij(n; T; f)
t:T. Dec(B(t))
Fin({t:T| B(t) })Propt:T. Dec(B(t)) Fin({t:T| B(t) })f:(nT). Bij(n; T; f)t:T. Dec(B(t)) Fin({t:T| B(t) })
