p:{p:(
)| 
i:. p(i) }.
Thm* (least i:
. p(i)) 
{i:| p(i) & (j:. j<i 
p(j)) }k:, p:{p:(k)| i:k. p(i) }.
Thm* (least i:
. p(i)) {i:k| p(i) & (j:i. p(j)) }| Theorem | Name |
| p:{p:()| i:. p(i) }.
Thm* (least i: . p(i)) {i:| p(i) & (j:. j<i p(j)) } | [least_characterized2] |
| cites the following: | |
| k:, p:{p:(k)| i:k. p(i) }.
Thm* (least i: . p(i)) {i:k| p(i) & (j:i. p(j)) } | [least_characterized] |