Nuprl - Pf set_function 1

PrintForm Definitions finite sets Sections AutomataTheory Doc

1. S: Type
2. T: Type
3. R: STProp
4. 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))

By: Inst Thm* Q:(ABProp). (x:A. y:B. Q(x,y)) (f:(AB). x:A. Q(x,f(x))) [{s:S| t:T. R(s,t) };T;x,y. R(x,y)]

Generated subgoals:

1 x:{s:S| t:T. R(s,t) }. y:T. R(x,y)

2 5. f:({s:S| t:T. R(s,t) }T). x:{s:S| t:T. R(s,t) }. R(x,f(x))
f:({s:S| t:T. R(s,t) }T). s:{s:S| t:T. R(s,t) }. R(s,f(s))

About:

1	`x:{s:S\| t:T. R(s,t) }. y:T. R(x,y)`
2	5. `f:({s:S\| t:T. R(s,t) }T). x:{s:S\| t:T. R(s,t) }. R(x,f(x))` `f:({s:S\| t:T. R(s,t) }T). s:{s:S\| t:T. R(s,t) }. R(s,f(s))`