n:
, f:(n
). increasing(f;n) 
(i:n, j:i. f(j) 
(f(i)))i:(k-1). f(i) < f(i+1)
is mentioned by
| Thm* n:, f:(n). increasing(f;n) (i:n, j:i. f(j) (f(i))) | [increasing-implies2] |
In prior sections: mb nat mb list 1
Try larger context:
Graphs