(27steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub bij ooc invpair 1 3 2 1 1
1. a : 
2. (f.<f,y.least x:. f(x)=y>)  (a bij a)aa
3. (fg.fg/f,g. f)  (aa)a bij a
4. f : aa
5. g : aa
6. InvFuns(a;a;f;g)
  <f,y.least x:. f(x)=y> = <f,g>  aa
By: f  a onto a |
(y.least x:. f(x)=y)  aa |
InvFuns(a;a;f;y.least x:. f(x)=y)
Asserted

Generated subgoals:

1   f  a onto a
2 steps
2 7. f  a onto a
  (y.least x:. f(x)=y)  aa
1 step
3 7. f  a onto a
8. (y.least x:. f(x)=y)  aa
  InvFuns(a;a;f;y.least x:. f(x)=y)
6 steps
4 7. f  a onto a
8. (y.least x:. f(x)=y)  aa
9. InvFuns(a;a;f;y.least x:. f(x)=y)
  <f,y.least x:. f(x)=y> = <f,g>  aa
2 steps

About:
pairspreadnatural_numberlambdaapplyfunctionequalmember
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(27steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc