PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
inv
of
fin
is
fin
1
1
2
2
1
2
1
1
2
2
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)
7.
f@0:
{s:S|
t:T. f(t) = s }
T
8.
s:{s:S|
t:T. f(t) = s }. f(f@0(s)) = s
9.
b1:
T
10.
b2:
T
11.
f(b1) = f(b2)
f@0(f(b1)) = b2
x,y:T//(f(x) = f(y))
By:
Analyze
Generated subgoals:
1
f(b1)
{s:S|
t:T. f(t) = s }
2
f(f@0(f(b1))) = f(b2)
About:
f(b1) 
{s:S| 
t:T. f(t) = s } f(f@0(f(b1))) = f(b2)
S
s:S. Dec(t:T. f(t) = s)t:T. f(t) = s }Ts:{s:S| t:T. f(t) = s }. f(f@0(s)) = s f@0(f(b1)) = b2 x,y:T//(f(x) = f(y)) f(b1) {s:S| t:T. f(t) = s } f(f@0(f(b1))) = f(b2)
