int
2
Sections
StandardLIB
Doc
Def
imin(a;b) == if a
b
a else b fi
is mentioned by
Thm*
a,b:
. (a -- (a -- b)) = imin(a;b)
[ndiff_ndiff_eq_imin]
Thm*
a,b,c:
. a
imin(b;c)
a
b & a
c
[imin_ub]
Thm*
a,b,c:
. imin(a;b)
c
a
c
b
c
[imin_lb]
Thm*
a,b,c:
. imin(a;b)+c = imin(a+c;b+c)
[imin_add_r]
Thm*
a,b:
. imin(a;b) = imin(b;a)
[imin_com]
Thm*
a,b,c:
. imin(a;imin(b;c)) = imin(imin(a;b);c)
[imin_assoc]
Thm*
a,b:
. -imin(a;b) = imax(-a;-b)
[minus_imin]
Thm*
a,b:
. -imax(a;b) = imin(-a;-b)
[minus_imax]
Try larger context:
StandardLIB
int
2
Sections
StandardLIB
Doc