Nuprl - Proof: compose iter inverses 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose iter inverses 1

1. A : Type

f,g:(A

A). InvFuns(A;A;f;g)

(

. InvFuns(A;A;f{

i};g{

i}))

By:	f,g:(AA). InvFuns(A;A;f;g) (i:, x:A. g{i}(f{i}(x)) = x) Asserted

Generated subgoals:

1 2. f : AA
3. g : AA
4. InvFuns(A;A;f;g)
5. i :
6. x : A
  g{i}(f{i}(x)) = x
6 steps

2 2. f,g:(AA). InvFuns(A;A;f;g)  (i:, x:A. g{i}(f{i}(x)) = x)
3. f : AA
4. g : AA
5. InvFuns(A;A;f;g)
6. i :
  InvFuns(A;A;f{i};g{i})
4 steps

About:

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

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

1	2. f : AA 3. g : AA 4. InvFuns(A;A;f;g) 5. i : 6. x : A g{i}(f{i}(x)) = x	6 steps
2	2. f,g:(AA). InvFuns(A;A;f;g) (i:, x:A. g{i}(f{i}(x)) = x) 3. f : AA 4. g : AA 5. InvFuns(A;A;f;g) 6. i : InvFuns(A;A;f{i};g{i})	4 steps