k,m:
, f:(k
m), g:(m
).
Thm* increasing(f;k)
increasing(g;m) increasing(g o f;k)k:, f:(k). increasing(f;k) (x,y:k. x<y f(x)<f(y))| Theorem | Name |
| k,m:, f:(km), g:(m).
Thm* increasing(f;k) increasing(g;m) increasing(g o f;k) | [compose_increasing] |
| cites the following: | |
| k:, f:(k). increasing(f;k) (x,y:k. x<y f(x)<f(y)) | [increasing_implies] |