(36steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one one corr rel vs invfuns 1
1. A : Type
2. B : Type
3. R : ABProp
  (1-1-Corr x:A,y:B. R(x;y))
  
  (f:(AB), g:(BA).
  (InvFuns(A;B;f;g) & (x:A, y:B. R(x;y)  y = f(x) & x = g(y)))
By: 2 Times Analyze

Generated subgoals:

1 4. 1-1-Corr x:A,y:B. R(x;y)
  f:(AB), g:(BA).
  InvFuns(A;B;f;g) & (x:A, y:B. R(x;y)  y = f(x) & x = g(y))
24 steps
2 4. f:(AB), g:(BA).
4. InvFuns(A;B;f;g) & (x:A, y:B. R(x;y)  y = f(x) & x = g(y))
  1-1-Corr x:A,y:B. R(x;y)
10 steps

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

(36steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc