Nuprl - Proof: nsub discr range surj 1 2 1 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub discr range surj 1 2 1 1

1. A : Type
2. A Discrete
3. k :

4. f :

k

A
5. {a:A|

i:

k. a = f(i) }

Type
6. f

k

{a:A|

i:

k. a = f(i) }
7. b : A
8.

i:

k. b = f(i) [not for witness]

a:

k. f(a) = b

{a:A|

i:

k. a = f(i)

A }

By:	FwdThru: Thm* (A Discrete) (e:(AA). x,y:A. (x e y) x = y) on [ A Discrete ] THEN Analyze-1

Generated subgoal:

1 9. e : AA
10. x,y:A. (x e y) x = y
a:k. f(a) = b {a:A| i:k. a = f(i) A }
9 steps

About:

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

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