a,b:
. (a -- (a -- b)) = imin(a;b)a,b:
. a+b = b+aa,b:. -imax(a;b) = imin(-a;-b)a,b,c:. imin(a;b)+c = imin(a+c;b+c)a,b:. imin(a;b) = imin(b;a)| Rank | Theorem | Name |
| 2 |
Thm* a,b:. (a -- (a -- b)) = imin(a;b) | [ndiff_ndiff_eq_imin] |
| cites | ||
| 0 | Thm* a,b:. a+b = b+a | [add_com] |
| 0 |
Thm* a,b:. -imax(a;b) = imin(-a;-b) | [minus_imax] |
| 1 |
Thm* a,b,c:. imin(a;b)+c = imin(a+c;b+c) | [imin_add_r] |
| 0 |
Thm* a,b:. imin(a;b) = imin(b;a) | [imin_com] |