| Who Cites increasing? |
|
increasing | Def increasing(f;k) == i:(k-1). f(i)<f(i+1) |
| | Thm* k:, f:(k). increasing(f;k) Prop |
|
int_seg | Def {i..j} == {k:| i k < j } |
| | Thm* m,n:. {m..n} Type |
|
lelt | Def i j < k == ij & j<k |
|
le | Def AB == B<A |
| | Thm* i,j:. (ij) Prop |
|
not | Def A == A False |
| | Thm* A:Prop. (A) Prop |