a,b,c:
. imin(a;b)+c = imin(a+c;b+c)i,j:. i = j 
-i = -ja,b:. a+b = b+aa,b:. -imin(a;b) = imax(-a;-b)a,b,c:. imax(a;b)+c = imax(a+c;b+c)| Theorem | Name |
|
Thm* a,b,c:. imin(a;b)+c = imin(a+c;b+c) | [imin_add_r] |
| cites | |
| Thm* i,j:. i = j -i = -j | [minus_mono_wrt_eq] |
| Thm* a,b:. a+b = b+a | [add_com] |
|
Thm* a,b:. -imin(a;b) = imax(-a;-b) | [minus_imin] |
|
Thm* a,b,c:. imax(a;b)+c = imax(a+c;b+c) | [imax_add_r] |