Reqmnts, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Basic Properties of Real Numbers --- Requirements

**by****Library Committee**- Received February 27, 2003
- MML identifier: REAL

- [ Mizar article, MML identifier index ]

environ vocabulary XREAL_0, ARYTM, ARYTM_3, ASYMPT_0, ZF_LANG, ARYTM_2, BOOLE; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ARYTM_2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0; constructors ARYTM_0, XREAL_0, ARYTM_2, XCMPLX_0, XBOOLE_0; clusters XREAL_0, ARYTM_2, NUMBERS, XCMPLX_0, ARYTM_3, ZFMISC_1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE; begin :: This file contains statements which are obvious for Mizar checker if :: "requirements REAL" is included in the environment description of an article. :: They are published for testing purposes only. :: Users should use appropriate requirements instead of referencing :: to these theorems. :: Note that the checker needs also "requirements BOOLE" to accept :: the statements with attribute 'zero'. reserve x, y, z for real number; theorem :: REAL:1 x <= y & x is positive implies y is positive; theorem :: REAL:2 x <= y & y is negative implies x is negative; theorem :: REAL:3 x <= y & x is non negative implies y is non negative; theorem :: REAL:4 x <= y & y is non positive implies x is non positive; theorem :: REAL:5 x <= y & y is non zero & x is non negative implies y is positive; theorem :: REAL:6 x <= y & x is non zero & y is non positive implies x is negative; theorem :: REAL:7 not x <= y & x is non positive implies y is negative; theorem :: REAL:8 not x <= y & y is non negative implies x is positive;

Back to top