| Who Cites complete intseg mset? |
|
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) |
|
lelt_int | Def i j < k == (ij)(j<k) |
| | Thm* i,j,k:. i j < k |
|
le_int | Def ij == j<i |
| | Thm* i,j:. (ij) |
|
lt_int | Def i<j == if i<j true ; false fi |
| | Thm* i,j:. (i<j) |
|
band | Def pq == if p q else false fi |
| | Thm* p,q:. (pq) |
|
bnot | Def b == if b false else true fi |
| | Thm* b:. b |