:: Subsets of Complex Numbers :: by Andrzej Trybulec :: :: Received November 7, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ORDINAL1, TARSKI, SUBSET_1, ARYTM_3, XBOOLE_0, CARD_1, ARYTM_2, ZFMISC_1, FUNCT_2, FUNCT_1, FUNCOP_1, RELAT_1, ORDINAL2, ORDINAL3, FINSET_1, NUMBERS; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1, ORDINAL2, ORDINAL3, FINSET_1, ARYTM_3, ARYTM_2; constructors FUNCT_4, ORDINAL3, ARYTM_2, FINSET_1, XTUPLE_0; registrations XBOOLE_0, ORDINAL1, FUNCT_2, ARYTM_3, ARYTM_2, RELAT_1, ORDINAL2, ORDINAL3, CARD_1; requirements BOOLE, SUBSET, NUMERALS; begin notation synonym NAT for omega; end; definition func REAL -> set equals :: NUMBERS:def 1 REAL+ \/ [:{0},REAL+:] \ {[0,0]}; end; registration cluster REAL -> non empty; end; definition func COMPLEX -> set equals :: NUMBERS:def 2 Funcs({0,1},REAL) \ { x where x is Element of Funcs({0,1 },REAL): x.1 = 0} \/ REAL; func RAT -> set equals :: NUMBERS:def 3 RAT+ \/ [:{0},RAT+:] \ {[0,0]}; func INT -> set equals :: NUMBERS:def 4 NAT \/ [:{0},NAT:] \ {[0,0]}; ::: redefine func NAT -> Subset of REAL; ::: coherence by Lm3,ARYTM_2:2,XBOOLE_1:1; end; registration 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; definition redefine func 0 -> Element of omega; end; 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; definition func ExtREAL -> set equals :: NUMBERS:def 5 REAL \/ { REAL, [0,REAL] }; end; registration cluster ExtREAL -> non empty; end; theorem :: NUMBERS:31 REAL c= ExtREAL; theorem :: NUMBERS:32 REAL <> ExtREAL; theorem :: NUMBERS:33 REAL c< ExtREAL; registration cluster INT -> infinite; cluster RAT -> infinite; cluster REAL -> infinite; cluster COMPLEX -> infinite; end;