Nuprl - Proof: inv pair functionality wrt one one corr 1

(13steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inv pair functionality wrt one one corr 1

1. A : Type
2. A' : Type
3. B : Type
4. B' : Type
5. A ~ A'
6. B ~ B'

B) ~ (A'

B')

By:	Analyze-2 THEN Analyze-2 THEN Analyze-2 THEN New:f' Analyze-1 THEN New:g' Analyze-1 THEN Analyze-1 THEN Def

Generated subgoal:

1 5. f : AA'
6. g : A'A
7. x:A. g(f(x)) = x
8. y:A'. f(g(y)) = y
9. f' : BB'
10. g' : B'B
11. x:B. g'(f'(x)) = x
12. y:B'. f'(g'(y)) = y
f:((AB)A'B'), g:((A'B')AB). InvFuns(AB;A'B';f;g)
11 steps

About:

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

(13steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc