:: Subsets of Complex Numbers
:: by Andrzej Trybulec
::
:: Received November 7, 2003
:: Copyright (c) 2003-2017 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;