PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
inv
of
fin
is
fin
1
1
2
2
1
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)
7.
s:
S
Dec(
t:T. (
s,t. f(t) = s)(s,t))
By:
Reduce 0
Generated subgoals:
None
About:
S
s:S. Dec(
t:T. f(t) = s)
Dec(t:T. (
s,t. f(t) = s)(s,t))
