n:
, f:(n
). increasing(f;n) 
(i:n, j:i. f(j) 
(f(i)))k:, f:(k
). increasing(f;k) (x,y:k. x < y f(x) < f(y))| Theorem | Name |
| Thm* n:, f:(n). increasing(f;n) (i:n, j:i. f(j) (f(i))) | [increasing-implies2] |
| cites | |
| Thm* k:, f:(k). increasing(f;k) (x,y:k. x < y f(x) < f(y)) | [increasing_implies] |