PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
finite
decidable
subset
1
1
2
1.
T:
Type
2.
B:
T
Prop
3.
n:
4.
f:(
n
T). Bij(
n; T; f)
5.
t:T. Dec(B(t))
6.
m:
.
m ~ {t:T| B(t) }
Fin({t:T| B(t) })
By:
Unfold `finite` 0
Generated subgoal:
1
n:
, f:(
n
{t:T| B(t) }). Bij(
n; {t:T| B(t) }; f)
About:
n:
, f:(n
{t:T| B(t) }). Bij(n; {t:T| B(t) }; f)Propf:(nT). Bij(n; T; f)
t:T. Dec(B(t))m:. m ~ {t:T| B(t) } Fin({t:T| B(t) }) n:, f:(n{t:T| B(t) }). Bij(n; {t:T| B(t) }; f)
