Nuprl - Proof: least exists 1 1 2 1 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: least exists 1 1 2 1 1

1. k :

2. P :

k

Prop
3.

i:

k. P(i)
4. p :

k

5.

i:

k. p(i)

P(i)
6. (least i:

. p(i))

{i:

k| p(i) & (

j:

i.

p(j)) }
7. u : {i:

k| p(i) & (

j:

i.

p(j)) }

u

{i:

k| P(i) & (

j:

i.

P(j)) }

By:	Analyze-1 THEN Analyze

Generated subgoal:

1 7. u : k
8. p(u) & (j:u. p(j))
P(u) & (j:u. P(j))
1 step

About:

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

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