| Some definitions of interest. |
|
complete_intseg_mset | Def complete_intseg_mset(a; b; f)(x) == if a x < b f(x) else 0 fi |
| | Thm* a,b:, f:({a..b}). complete_intseg_mset(a; b; f) |
|
int_seg | Def {i..j} == {k:| i k < j } |
| | Thm* m,n:. {m..n} Type |
|
nat | Def == {i:| 0i } |
| | Thm* Type |