Nuprl - Proof: nsub surj imp a rev inj gen 1 1 3 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub surj imp a rev inj gen 1 1 3 1

1. B : Type
2. e : B

B

3. IsEqFun(B;e)
4. a :

5. f :

a

B
6. Surj(

a; B; f)
7. f

a onto

B
8. (

y,x. (f(x)) e y)

B

{p:(

a

)|

i:

a. p(i) }
9. (

y.least x:

. (f(x)) e y)

B

a

Inj(B;

a;

y.least x:

. (f(x)) e y)

By:	((New:i1 Analyze) THEN (New:i2 Analyze)) THEN Reduce Hyp:-1

Generated subgoal:

1 10. i1 : B
11. i2 : B
12. (least x:. (f(x)) e i1) = (least x:. (f(x)) e i2) a
i1 = i2
4 steps

About:

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

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