PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Computing the inverse of a finite function

At: nsub surj least preimage total

  b,a:, f:(a onto b), y:b. (least x:. f(x)=y)  a
By: Analyze
THEN
Use:[B:= b | e(i,j):= i=j]
Inst: 
Thm*  e:(BB). 
Thm*  IsEqFun(B;e)  (a:, f:(a onto B), y:B. (least x:. (f(x)) e y)  a)
THEN
BackThru: Thm*  IsEqFun(b;i,j. i=j)

Generated subgoals:

None

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

PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc