PrintForm Definitions finite sets Sections AutomataTheory Doc

At: inv of fin is fin 1 1 2 2 1 2 1 1 2 2 1 2 3 1
1. T: Type
2. S: Type
3. f: TS
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. b: x,y:T//(f(x) = f(y))

* = * (t:T. f(t) = f(b))
By: Analyze 9
Generated subgoals:

19. b1: T
10. b2: T
f(b1) = f(b2) Type
2 (t:T. f(t) = f(b)) Type
39. b1: T
10. b2: T
11. f(b1) = f(b2)
* = * (t:T. f(t) = f(b1))

About:
equalexistsapplyaxiomuniverse
functionallsetquotientmember