PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
quotient
of
finite
1
1.
n:
{1...}
2.
A:
Type
3.
R:
A
A
Prop
4.
n ~ A
5.
EquivRel x,y:A. x R y
6.
x,y:A. Dec(x R y)
m:
(n+1).
m ~ (x,y:A//(x R y))
By:
FwdThru
Thm*
(
f:(A
B). Bij(A; B; f))
(A ~ B) [4]
THEN
Analyze -1
Generated subgoal:
1
7.
f:
n
A
8.
Bij(
n; A; f)
m:
(n+1).
m ~ (x,y:A//(x R y))
About:
n
An; A; f)
m:(n+1). m ~ (x,y:A//(x R y))APropn ~ A
x,y:A. Dec(x R y) m:(n+1). m ~ (x,y:A//(x R y))f:(AB). Bij(A; B; f)) 
(A ~ B)
[4]
nAn; A; f) m:(n+1). m ~ (x,y:A//(x R y))
