(14steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: injection type functionality wrt ooc 1
1. A : Type
2. A' : Type
3. B : Type
4. B' : Type
5. A ~ A'
6. B ~ B'
  (A inj B) ~ (A' inj B')
By: Analyze A ~ A' and B ~ B' and extract facts about cancellation and injection.

Generated subgoal:

1 5. f1 : AA'
6. g1 : A'A
7. InvFuns(A;A';f1;g1)
8. f : BB'
9. g : B'B
10. InvFuns(B;B';f;g)
11. x:B. g(f(x)) = x
12. y:B'. f(g(y)) = y
13. x:A. g1(f1(x)) = x
14. y:A'. f1(g1(y)) = y
15. Inj(A; A'; f1)
16. Inj(A'; A; g1)
17. Inj(B; B'; f)
18. Inj(B'; B; g)
  (A inj B) ~ (A' inj B')
12 steps

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

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