Nuprl - Pf inv_of_fin_is_fin 1 1 2 2 1 2 1 1 2 2

PrintForm Definitions finite sets Sections AutomataTheory Doc

At: inv of fin is fin 1 1 2 2 1 2 1 1 2 2

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))

a:{s:S| t:T. f(t) = s }. f@0(a) = b x,y:T//(f(x) = f(y))

By: Witness f(b)

Generated subgoals:

1 f(b) {s:S| t:T. f(t) = s }

2 f@0(f(b)) = b x,y:T//(f(x) = f(y))

3 10. a: {s:S| t:T. f(t) = s }
f@0(a) = b x,y:T//(f(x) = f(y)) Prop

About:

1	`f(b) {s:S\| t:T. f(t) = s }`
2	`f@0(f(b)) = b x,y:T//(f(x) = f(y))`
3	10. `a:` `{s:S\| t:T. f(t) = s }` `f@0(a) = b x,y:T//(f(x) = f(y)) Prop`