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

PrintForm Definitions finite sets Sections AutomataTheory Doc

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

f1:({s:S| t:T. f(t) = s }(x,y:T//(f(x) = f(y)))). Bij({s:S| t:T. f(t) = s }; x,y:T//(f(x) = f(y)); f1)

By: Witness f@0

Generated subgoals:

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

2 Bij({s:S| t:T. f(t) = s }; x,y:T//(f(x) = f(y)); f@0)

3 9. f1: {s:S| t:T. f(t) = s }(x,y:T//(f(x) = f(y)))
Bij({s:S| t:T. f(t) = s }; x,y:T//(f(x) = f(y)); f1) Prop

About:

1	`f@0 {s:S\| t:T. f(t) = s }(x,y:T//(f(x) = f(y)))`
2	`Bij({s:S\| t:T. f(t) = s }; x,y:T//(f(x) = f(y)); f@0)`
3	9. `f1:` `{s:S\| t:T. f(t) = s }(x,y:T//(f(x) = f(y)))` `Bij({s:S\| t:T. f(t) = s }; x,y:T//(f(x) = f(y)); f1) Prop`