Nuprl - Pf inv_of_fin_is

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)

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: Inst Thm* R:(STProp). (s:S. Dec(t:T. R(s,t))) (f:({s:S| t:T. R(s,t) }T). s:{s:S| t:T. R(s,t) }. R(s,f(s))) [S;T;s,t. f(t) = s]

Generated subgoals:

1 7. s: S
Dec(t:T. (s,t. f(t) = s)(s,t))

2 7. f@0:({s:S| t:T. (s,t. f(t) = s)(s,t) }T). s:{s:S| t:T. (s,t. f(t) = s)(s,t) }. (s,t. f(t) = s)(s,f@0(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)

About:

1	7. `s:` `S` `Dec(t:T. (s,t. f(t) = s)(s,t))`
2	7. `f@0:({s:S\| t:T. (s,t. f(t) = s)(s,t) }T). s:{s:S\| t:T. (s,t. f(t) = s)(s,t) }. (s,t. f(t) = s)(s,f@0(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)`