PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
inv
of
fin
is
fin
1
1
2
1
1.
T:
Type
2.
S:
Type
3.
f:
T
S
4.
Fin(S)
5.
s:S. Dec(
t:T. f(t) = s)
6.
EquivRel x,y:T. f(x) = f(y)
Fin({s:S|
t:T. f(t) = s })
By:
Inst
Thm*
B:(T
Prop). Fin(T) & (
t:T. Dec(B(t)))
Fin({t:T| B(t) }) [S;
s.
t:T. f(t) = s]
Generated subgoals:
1
7.
t:
S
Dec((
s.
t:T. f(t) = s)(t))
2
7.
Fin({t:S| (
s.
t:T. f(t) = s)(t) })
Fin({s:S|
t:T. f(t) = s })
About: