(2steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: least satisfies 1

1. k : 
2. p : {p:(k)| i:k. p(i) }
3. (least i:. p(i))  {i:k| p(i) & (j:i. p(j)) }
  p(least i:. p(i))


By: Analyze3 THEN Analyze2 THEN Unhide


Generated subgoals:

None

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

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