(10steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Characterization of "least".

At: least characterized2

  p:{p:()| i:. p(i) }. 
  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }
By: UnivCD

Generated subgoal:

1 1. p : {p:()| i:. p(i) }
  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }
9 steps

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

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