Addenda , 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Subsets of Complex Numbers

**by****Andrzej Trybulec**- Received November 7, 2003
- MML identifier: NUMBERS

- [ Mizar article, MML identifier index ]

environ vocabulary COMPLEX1, FUNCT_2, FUNCT_1, FUNCOP_1, ARYTM_2, BOOLE, ARYTM_3, ORDINAL2, ARYTM, ORDINAL1, RELAT_1, RAT_1, INT_1, ORDINAL3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1, ORDINAL2, ORDINAL3, ARYTM_3, ARYTM_2; constructors ARYTM_1, FRAENKEL, FUNCT_4, ORDINAL3; clusters XBOOLE_0, ARYTM_2, SUBSET_1, ORDINAL2, ARYTM_3, FRAENKEL, FUNCT_2, FUNCT_4, ORDINAL1, ZFMISC_1; requirements BOOLE, SUBSET, NUMERALS; begin definition func REAL equals :: NUMBERS:def 1 REAL+ \/ [:{0},REAL+:] \ {[0,0]}; redefine func omega; synonym NAT; end; definition cluster REAL -> non empty; end; definition func COMPLEX equals :: NUMBERS:def 2 Funcs({0,one},REAL) \ { x where x is Element of Funcs({0,one},REAL): x.one = 0} \/ REAL; func RAT equals :: NUMBERS:def 3 RAT+ \/ [:{0},RAT+:] \ {[0,0]}; func INT equals :: NUMBERS:def 4 NAT \/ [:{0},NAT:] \ {[0,0]}; redefine func NAT -> Subset of REAL; end; definition cluster COMPLEX -> non empty; cluster RAT -> non empty; cluster INT -> non empty; end; reserve i,j,k for Element of NAT; reserve a,b for Element of REAL; theorem :: NUMBERS:1 REAL c< COMPLEX; reserve r,s,t for Element of RAT+; reserve i,j,k for Element of omega; theorem :: NUMBERS:2 RAT c< REAL; theorem :: NUMBERS:3 RAT c< COMPLEX; theorem :: NUMBERS:4 INT c< RAT; theorem :: NUMBERS:5 INT c< REAL; theorem :: NUMBERS:6 INT c< COMPLEX; theorem :: NUMBERS:7 NAT c< INT; theorem :: NUMBERS:8 NAT c< RAT; theorem :: NUMBERS:9 NAT c< REAL; theorem :: NUMBERS:10 NAT c< COMPLEX; begin :: to be canceled theorem :: NUMBERS:11 REAL c= COMPLEX; theorem :: NUMBERS:12 RAT c= REAL; theorem :: NUMBERS:13 RAT c= COMPLEX; theorem :: NUMBERS:14 INT c= RAT; theorem :: NUMBERS:15 INT c= REAL; theorem :: NUMBERS:16 INT c= COMPLEX; theorem :: NUMBERS:17 NAT c= INT; theorem :: NUMBERS:18 NAT c= RAT; theorem :: NUMBERS:19 NAT c= REAL; theorem :: NUMBERS:20 NAT c= COMPLEX; theorem :: NUMBERS:21 REAL <> COMPLEX; theorem :: NUMBERS:22 RAT <> REAL; theorem :: NUMBERS:23 RAT <> COMPLEX; theorem :: NUMBERS:24 INT <> RAT; theorem :: NUMBERS:25 INT <> REAL; theorem :: NUMBERS:26 INT <> COMPLEX; theorem :: NUMBERS:27 NAT <> INT; theorem :: NUMBERS:28 NAT <> RAT; theorem :: NUMBERS:29 NAT <> REAL; theorem :: NUMBERS:30 NAT <> COMPLEX;

Back to top