| 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 == (i j) (j< k) |
| | Thm* i,j,k: . i  j < k  |
|
le_int | Def i j ==  j< i |
| | Thm* i,j: . (i j)  |
|
lt_int | Def i< j == if i<j true ; false fi |
| | Thm* i,j: . (i< j)  |
|
band | Def p q == if p q else false fi |
| | Thm* p,q: . (p q)  |
|
bnot | Def  b == if b false else true fi |
| | Thm* b: .  b  |