k:
, p:{p:(k
)| 
i:k. p(i) }. p(least i:. p(i))k:, p:{p:(k)| i:k. p(i) }.
Thm* (least i:
. p(i)) 
{i:k| p(i) & (j:i. 
p(j)) }| Theorem | Name |
| k:, p:{p:(k)| i:k. p(i) }. p(least i:. p(i)) | [least_satisfies] |
| 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] |