(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:kp(i) }
3. (least i:p(i))  {i:kp(i) & (j:ip(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