(36steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Equivalence of one-one correspondence and existence of inverses

At: one one corr rel vs invfuns

  A,B:Type, 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: UnivCD

Generated subgoal:

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)))
35 steps

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

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