Nuprl - Proof: pigeon hole 1

(8steps total) Remark PfGloss PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pigeon hole 1

1. m :

2. k :

3. f :

m

k
4. k<m

x,y:

m. x

y & f(x) = f(y)

By:	Inst: Thm* m:, f:(m). Inj(m; ; f) (x:m, y:x. f(x) = f(y)) on [m \| f]

Generated subgoals:

1 Inj(m; ; f)
5 steps

2 5. x:m, y:x. f(x) = f(y)
x,y:m. x y & f(x) = f(y)
1 step

About:

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

(8steps total) Remark PfGloss PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc