PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
inv
of
fin
is
fin
1
1
1.
T:
Type
2.
S:
Type
3.
f:
T
S
4.
Fin(S)
5.
s:S. Dec(
t:T. f(t) = s)
Fin(x,y:T//(f(x) = f(y)))
By:
Assert (EquivRel x,y:T. f(x) = f(y))
Generated subgoals:
1
EquivRel x,y:T. f(x) = f(y)
2
6.
EquivRel x,y:T. f(x) = f(y)
Fin(x,y:T//(f(x) = f(y)))
About:
EquivRel x,y:T. f(x) = f(y) Fin(x,y:T//(f(x) = f(y)))
S
s:S. Dec(
t:T. f(t) = s) Fin(x,y:T//(f(x) = f(y))) EquivRel x,y:T. f(x) = f(y) Fin(x,y:T//(f(x) = f(y)))
