Nuprl - Proof: least exists2 1 1

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

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

1. P :

Prop
2.

i:

. P(i) [not for witness]
3. p :

4.

i:

. p(i)

P(i)

{i:

| P(i) & (

j:

. j<i

P(j)) }

By:	Inst: Thm* p:{p:()\| i:. p(i) }. Thm* (least i:. p(i)) {i:\| p(i) & (j:. j<i p(j)) } Using:[p]

Generated subgoals:

1 2. i:. P(i)
3. p :
4. i:. p(i)  P(i)
  p  {p:()| i:. p(i) }
2 steps

2 5. (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }
  {i:| P(i) & (j:. j<i  P(j)) }
4 steps

About:

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

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