(4steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: left inv of surj is right inv 1

1. A : Type
2. B : Type
3. f : AB
4. g : BA
5. Surj(ABf)
6. x:Ag(f(x)) = x
7. y : B
  f(g(y)) = y


By: Witness5: y THEN Analyze-1


Generated subgoal:

1 8. a : A
9. f(a) = y
  f(g(y)) = y

2 steps

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

(4steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc