PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
quotient
1
1
corr
1
1
1
1
1
1.
A:
Type
2.
B:
Type
3.
f:
A
B
4.
R:
B
B
Prop
5.
Bij(A; B; f)
6.
EquivRel x,y:B. x R y
7.
EquivRel x,y:A. x R_f y
8.
g:
B
A
9.
InvFuns(A; B; f; g)
10.
x:
x,y:A//(x R_f y)
f(x)
x,y:B//(x R y)
By:
Analyze -1
Generated subgoal:
1
10.
x1:
A
11.
x2:
A
12.
x1 R_f x2
f(x1) = f(x2)
x,y:B//(x R y)
About:
f(x1) = f(x2) 
x,y:B//(x R y)
BBPropA f(x) x,y:B//(x R y) f(x1) = f(x2) x,y:B//(x R y)
