PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quotient of finite 1 1 1 1 1
1. n: {1...}
2. A: Type
3. R: AAProp
4. n ~ A
5. EquivRel x,y:A. x R y
6. x,y:A. Dec(x R y)
7. f: nA
8. Bij(n; A; f)
9. F:((x,y:n//(x R_f y))(x,y:A//(x R y))). Bij(x,y:n//(x R_f y); x,y:A//(x R y); F)
10. EquivRel x,y:n. x R_f y
11. (x,y:n//(x R_f y)) ~ (x,y:A//(x R y))

m:(n+1). m ~ (x,y:A//(x R y))
By: Inst Thm* n:{1...}, E:(nnProp). (EquivRel x,y:n. x E y) & (x,y:n. Dec(x E y)) (m:(n+1). m ~ (i,j:n//(i E j))) [n;R_f]
Generated subgoals:

112. x: n
13. y: n
Dec(x R_f y)
212. m:(n+1). m ~ (i,j:n//(i R_f j))
m:(n+1). m ~ (x,y:A//(x R y))

About:
existsnatural_numberaddquotientuniversefunctionpropall