Nuprl - Proof: nsub discr range surj 1 2 1 1 1 2 1 1 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 2 1 1 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)
9. e : A

A

10.

x,y:A. (x e y)

x = y
11. (

j.(f(j)) e b)

{p:(

k

)|

i:

k. p(i) }
12. (least i:

. (f(i)) e b)

k
13. (f(least i:

. (f(i)) e b)) e b
14. f(least i:

. (f(i)) e b) = b

i:

k. f(least i:

. (f(i)) e b) = f(i)

By:	SimilarTo: i:k. b = f(i)

Generated subgoals:

None

About:

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

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