Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Some Properties of Functions Modul and Signum

**by****Jan Popiolek**- Received June 21, 1989
- MML identifier: ABSVALUE

- [ Mizar article, MML identifier index ]

environ vocabulary ARYTM, ARYTM_1, ARYTM_3, RELAT_1, ABSVALUE; notation ORDINAL1, XCMPLX_0, XREAL_0, REAL_1; constructors REAL_1, XCMPLX_0, XREAL_0, XBOOLE_0; clusters XREAL_0, REAL_1, ARYTM_3, ZFMISC_1, XBOOLE_0; requirements REAL, NUMERALS, SUBSET, ARITHM; begin reserve x, y, z, s, t for real number; definition let x; func abs x -> real number equals :: ABSVALUE:def 1 x if 0 <= x otherwise -x; projectivity; end; definition let x be Real; redefine func abs x -> Real; end; canceled 4; theorem :: ABSVALUE:5 0 <= abs(x); theorem :: ABSVALUE:6 x <> 0 implies 0 < abs(x); theorem :: ABSVALUE:7 x = 0 iff abs(x) = 0; canceled; theorem :: ABSVALUE:9 abs(x) = -x & x <> 0 implies x < 0; theorem :: ABSVALUE:10 abs(x*y) = abs(x) * abs(y); theorem :: ABSVALUE:11 -abs(x) <= x & x <= abs(x); theorem :: ABSVALUE:12 -y <= x & x <= y iff abs(x) <= y; theorem :: ABSVALUE:13 abs(x+y) <= abs(x) + abs(y); theorem :: ABSVALUE:14 x <> 0 implies abs(x) * abs(1/x) = 1; theorem :: ABSVALUE:15 abs(1/x) = 1/abs(x); theorem :: ABSVALUE:16 abs(x/y) = abs(x)/abs(y); theorem :: ABSVALUE:17 abs(x) = abs(-x); theorem :: ABSVALUE:18 abs(x) - abs(y) <= abs(x-y); theorem :: ABSVALUE:19 abs(x-y) <= abs(x) + abs(y); canceled; theorem :: ABSVALUE:21 abs(x) <= z & abs(y) <= t implies abs(x+y) <= z + t; theorem :: ABSVALUE:22 abs(abs(x) - abs(y)) <= abs(x-y); canceled; theorem :: ABSVALUE:24 0 <= x * y implies abs(x+y) = abs(x) + abs(y); theorem :: ABSVALUE:25 abs(x+y) = abs(x) + abs(y) implies 0 <= x * y; theorem :: ABSVALUE:26 abs(x+y)/(1 + abs(x+y)) <= abs(x)/(1 + abs(x)) + abs(y)/(1 +abs(y)); definition let x; func sgn x equals :: ABSVALUE:def 2 1 if 0 < x, -1 if x < 0 otherwise 0; end; definition let x; cluster sgn x -> real; end; definition let x be Real; redefine func sgn x -> Real; end; canceled 4; theorem :: ABSVALUE:31 sgn x = 1 implies 0 < x; theorem :: ABSVALUE:32 sgn x = -1 implies x < 0; theorem :: ABSVALUE:33 sgn x = 0 implies x = 0; theorem :: ABSVALUE:34 x = abs(x) * sgn x; theorem :: ABSVALUE:35 sgn (x * y) = sgn x * sgn y; theorem :: ABSVALUE:36 sgn sgn x = sgn x; theorem :: ABSVALUE:37 sgn (x + y) <= sgn x + sgn y + 1; theorem :: ABSVALUE:38 x <> 0 implies sgn x * sgn (1/x) = 1; theorem :: ABSVALUE:39 1/(sgn x) = sgn (1/x); theorem :: ABSVALUE:40 sgn x + sgn y - 1 <= sgn ( x + y ); theorem :: ABSVALUE:41 sgn x = sgn (1/x); theorem :: ABSVALUE:42 sgn (x/y) = (sgn x)/(sgn y);

Back to top