Nuprl - Proof: inv funs iff inv funs 2 1

(8steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inv funs iff inv funs 2 1

A,B:Type, f:(A

B), g:(B

A).

g o f = Id & f o g = Id

(

x:A. g(f(x)) = x) & (

y:B. f(g(y)) = y)

By:	A,B:Type, f:(AB), g:(BA). g o f = Id (x:A. g(f(x)) = x) Asserted

Generated subgoals:

1   A,B:Type, f:(AB), g:(BA). g o f = Id  (x:A. g(f(x)) = x)
5 steps

2 1. A,B:Type, f:(AB), g:(BA). g o f = Id  (x:A. g(f(x)) = x)
  A,B:Type, f:(AB), g:(BA).
  g o f = Id & f o g = Id  (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y)
1 step

About:

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

(8steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

1	A,B:Type, f:(AB), g:(BA). g o f = Id (x:A. g(f(x)) = x)	5 steps
2	1. A,B:Type, f:(AB), g:(BA). g o f = Id (x:A. g(f(x)) = x) A,B:Type, f:(AB), g:(BA). g o f = Id & f o g = Id (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y)	1 step