a,b,c:
. imin(a;imin(b;c)) = imin(imin(a;b);c)a,b:. -imin(a;b) = imax(-a;-b)i,j:. i = j 
-i = -ja,b,c:. imax(a;imax(b;c)) = imax(imax(a;b);c)| Theorem | Name |
|
Thm* a,b,c:. imin(a;imin(b;c)) = imin(imin(a;b);c) | [imin_assoc] |
| cites | |
|
Thm* a,b:. -imin(a;b) = imax(-a;-b) | [minus_imin] |
| Thm* i,j:. i = j -i = -j | [minus_mono_wrt_eq] |
|
Thm* a,b,c:. imax(a;imax(b;c)) = imax(imax(a;b);c) | [imax_assoc] |