:: On the Sets Inhabited by Numbers
:: by Andrzej Trybulec
::
:: Received August 23, 2003
:: Copyright (c) 2003-2018 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 XCMPLX_0, XXREAL_0, XREAL_0, RAT_1, INT_1, ORDINAL1, NUMBERS,
XBOOLE_0, SUBSET_1, TARSKI, SETFAM_1, MEMBERED, IDEAL_1, ARYTM_3, NAT_1,
CARD_1, REAL_1;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, RAT_1, INT_1, NAT_1;
constructors ENUMSET1, SETFAM_1, XCMPLX_0, XXREAL_0, RAT_1, NUMBERS, NAT_1;
registrations XREAL_0, INT_1, RAT_1, ORDINAL1, XCMPLX_0, NAT_1, XBOOLE_0;
requirements BOOLE, SUBSET;
begin
reserve x for object, X, F for set;
definition
let X be set;
attr X is complex-membered means
:: MEMBERED:def 1
x in X implies x is complex;
attr X is ext-real-membered means
:: MEMBERED:def 2
x in X implies x is ext-real;
attr X is real-membered means
:: MEMBERED:def 3
x in X implies x is real;
attr X is rational-membered means
:: MEMBERED:def 4
x in X implies x is rational;
attr X is integer-membered means
:: MEMBERED:def 5
x in X implies x is integer;
attr X is natural-membered means
:: MEMBERED:def 6
x in X implies x is natural;
end;
registration
cluster natural-membered -> integer-membered for set;
cluster integer-membered -> rational-membered for set;
cluster rational-membered -> real-membered for set;
cluster real-membered -> ext-real-membered for set;
cluster real-membered -> complex-membered for set;
end;
registration
cluster non empty natural-membered for set;
end;
registration
cluster COMPLEX -> complex-membered;
cluster ExtREAL -> ext-real-membered;
cluster REAL -> real-membered;
cluster RAT -> rational-membered;
cluster INT -> integer-membered;
cluster NAT -> natural-membered;
end;
theorem :: MEMBERED:1
X is complex-membered implies X c= COMPLEX;
theorem :: MEMBERED:2
X is ext-real-membered implies X c= ExtREAL;
theorem :: MEMBERED:3
X is real-membered implies X c= REAL;
theorem :: MEMBERED:4
X is rational-membered implies X c= RAT;
theorem :: MEMBERED:5
X is integer-membered implies X c= INT;
theorem :: MEMBERED:6
X is natural-membered implies X c= NAT;
registration
let X be complex-membered set;
cluster -> complex for Element of X;
end;
registration
let X be ext-real-membered set;
cluster -> ext-real for Element of X;
end;
registration
let X be real-membered set;
cluster -> real for Element of X;
end;
registration
let X be rational-membered set;
cluster -> rational for Element of X;
end;
registration
let X be integer-membered set;
cluster -> integer for Element of X;
end;
registration
let X be natural-membered set;
cluster -> natural for Element of X;
end;
reserve c, c1, c2, c3 for Complex,
e, e1, e2, e3 for ExtReal,
r , r1, r2, r3 for Real,
w, w1, w2, w3 for Rational,
i, i1, i2, i3 for Integer,
n, n1, n2, n3 for Nat;
theorem :: MEMBERED:7
for X being non empty complex-membered set ex c st c in X;
theorem :: MEMBERED:8
for X being non empty ext-real-membered set ex e st e in X;
theorem :: MEMBERED:9
for X being non empty real-membered set ex r st r in X;
theorem :: MEMBERED:10
for X being non empty rational-membered set ex w st w in X;
theorem :: MEMBERED:11
for X being non empty integer-membered set ex i st i in X;
theorem :: MEMBERED:12
for X being non empty natural-membered set ex n st n in X;
theorem :: MEMBERED:13
for X being complex-membered set st for c holds c in X holds X = COMPLEX;
theorem :: MEMBERED:14
for X being ext-real-membered set st for e holds e in X holds X = ExtREAL;
theorem :: MEMBERED:15
for X being real-membered set st for r holds r in X holds X = REAL;
theorem :: MEMBERED:16
for X being rational-membered set st for w holds w in X holds X = RAT;
theorem :: MEMBERED:17
for X being integer-membered set st for i holds i in X holds X = INT;
theorem :: MEMBERED:18
for X being natural-membered set st for n holds n in X holds X = NAT;
theorem :: MEMBERED:19
for Y being complex-membered set st X c= Y holds X is complex-membered;
theorem :: MEMBERED:20
for Y being ext-real-membered set st X c= Y holds X is ext-real-membered;
theorem :: MEMBERED:21
for Y being real-membered set st X c= Y holds X is real-membered;
theorem :: MEMBERED:22
for Y being rational-membered set st X c= Y holds X is rational-membered;
theorem :: MEMBERED:23
for Y being integer-membered set st X c= Y holds X is integer-membered;
theorem :: MEMBERED:24
for Y being natural-membered set st X c= Y holds X is natural-membered;
registration
cluster empty -> natural-membered for set;
end;
registration
let c;
cluster {c} -> complex-membered;
end;
registration
let e be ExtReal;
cluster {e} -> ext-real-membered;
end;
registration
let r;
cluster {r} -> real-membered;
end;
registration
let w;
cluster {w} -> rational-membered;
end;
registration
let i;
cluster {i} -> integer-membered;
end;
registration
let n;
cluster {n} -> natural-membered;
end;
registration
let c1,c2;
cluster {c1,c2} -> complex-membered;
end;
registration
let e1,e2 be ExtReal;
cluster {e1,e2} -> ext-real-membered;
end;
registration
let r1,r2;
cluster {r1,r2} -> real-membered;
end;
registration
let w1,w2;
cluster {w1,w2} -> rational-membered;
end;
registration
let i1,i2;
cluster {i1,i2} -> integer-membered;
end;
registration
let n1,n2;
cluster {n1,n2} -> natural-membered;
end;
registration
let c1,c2,c3;
cluster {c1,c2,c3} -> complex-membered;
end;
registration
let e1,e2,e3 be ExtReal;
cluster {e1,e2,e3} -> ext-real-membered;
end;
registration
let r1,r2,r3;
cluster {r1,r2,r3} -> real-membered;
end;
registration
let w1,w2,w3;
cluster {w1,w2,w3} -> rational-membered;
end;
registration
let i1,i2,i3;
cluster {i1,i2,i3} -> integer-membered;
end;
registration
let n1,n2,n3;
cluster {n1,n2,n3} -> natural-membered;
end;
registration
let X be complex-membered set;
cluster -> complex-membered for Subset of X;
end;
registration
let X be ext-real-membered set;
cluster -> ext-real-membered for Subset of X;
end;
registration
let X be real-membered set;
cluster -> real-membered for Subset of X;
end;
registration
let X be rational-membered set;
cluster -> rational-membered for Subset of X;
end;
registration
let X be integer-membered set;
cluster -> integer-membered for Subset of X;
end;
registration
let X be natural-membered set;
cluster -> natural-membered for Subset of X;
end;
registration
let X,Y be complex-membered set;
cluster X \/ Y -> complex-membered;
end;
registration
let X,Y be ext-real-membered set;
cluster X \/ Y -> ext-real-membered;
end;
registration
let X,Y be real-membered set;
cluster X \/ Y -> real-membered;
end;
registration
let X,Y be rational-membered set;
cluster X \/ Y -> rational-membered;
end;
registration
let X,Y be integer-membered set;
cluster X \/ Y -> integer-membered;
end;
registration
let X,Y be natural-membered set;
cluster X \/ Y -> natural-membered;
end;
registration
let X be complex-membered set, Y be set;
cluster X /\ Y -> complex-membered;
cluster Y /\ X -> complex-membered;
end;
registration
let X be ext-real-membered set, Y be set;
cluster X /\ Y -> ext-real-membered;
cluster Y /\ X -> ext-real-membered;
end;
registration
let X be real-membered set, Y be set;
cluster X /\ Y -> real-membered;
cluster Y /\ X -> real-membered;
end;
registration
let X be rational-membered set, Y be set;
cluster X /\ Y -> rational-membered;
cluster Y /\ X -> rational-membered;
end;
registration
let X be integer-membered set, Y be set;
cluster X /\ Y -> integer-membered;
cluster Y /\ X -> integer-membered;
end;
registration
let X be natural-membered set, Y be set;
cluster X /\ Y -> natural-membered;
cluster Y /\ X -> natural-membered;
end;
registration
let X be complex-membered set, Y be set;
cluster X \ Y -> complex-membered;
end;
registration
let X be ext-real-membered set, Y be set;
cluster X \ Y -> ext-real-membered;
end;
registration
let X be real-membered set, Y be set;
cluster X \ Y -> real-membered;
end;
registration
let X be rational-membered set, Y be set;
cluster X \ Y -> rational-membered;
end;
registration
let X be integer-membered set, Y be set;
cluster X \ Y -> integer-membered;
end;
registration
let X be natural-membered set, Y be set;
cluster X \ Y -> natural-membered;
end;
registration
let X,Y be complex-membered set;
cluster X \+\ Y -> complex-membered;
end;
registration
let X,Y be ext-real-membered set;
cluster X \+\ Y -> ext-real-membered;
end;
registration
let X,Y be real-membered set;
cluster X \+\ Y -> real-membered;
end;
registration
let X,Y be rational-membered set;
cluster X \+\ Y -> rational-membered;
end;
registration
let X,Y be integer-membered set;
cluster X \+\ Y -> integer-membered;
end;
registration
let X,Y be natural-membered set;
cluster X \+\ Y -> natural-membered;
end;
definition
let X be complex-membered set, Y be set;
redefine pred X c= Y means
:: MEMBERED:def 7
c in X implies c in Y;
end;
definition
let X be ext-real-membered set, Y be set;
redefine pred X c= Y means
:: MEMBERED:def 8
e in X implies e in Y;
end;
definition
let X be real-membered set, Y be set;
redefine pred X c= Y means
:: MEMBERED:def 9
r in X implies r in Y;
end;
definition
let X be rational-membered set, Y be set;
redefine pred X c= Y means
:: MEMBERED:def 10
w in X implies w in Y;
end;
definition
let X be integer-membered set, Y be set;
redefine pred X c= Y means
:: MEMBERED:def 11
i in X implies i in Y;
end;
definition
let X be natural-membered set, Y be set;
redefine pred X c= Y means
:: MEMBERED:def 12
n in X implies n in Y;
end;
definition
let X,Y be complex-membered set;
redefine pred X = Y means
:: MEMBERED:def 13
c in X iff c in Y;
end;
definition
let X,Y be ext-real-membered set;
redefine pred X = Y means
:: MEMBERED:def 14
e in X iff e in Y;
end;
definition
let X,Y be real-membered set;
redefine pred X = Y means
:: MEMBERED:def 15
r in X iff r in Y;
end;
definition
let X,Y be rational-membered set;
redefine pred X = Y means
:: MEMBERED:def 16
w in X iff w in Y;
end;
definition
let X,Y be integer-membered set;
redefine pred X = Y means
:: MEMBERED:def 17
i in X iff i in Y;
end;
definition
let X,Y be natural-membered set;
redefine pred X = Y means
:: MEMBERED:def 18
n in X iff n in Y;
end;
definition
let X,Y be complex-membered set;
redefine pred X misses Y means
:: MEMBERED:def 19
not ex c st c in X & c in Y;
end;
definition
let X,Y be ext-real-membered set;
redefine pred X misses Y means
:: MEMBERED:def 20
not ex e st e in X & e in Y;
end;
definition
let X,Y be real-membered set;
redefine pred X misses Y means
:: MEMBERED:def 21
not ex r st r in X & r in Y;
end;
definition
let X,Y be rational-membered set;
redefine pred X misses Y means
:: MEMBERED:def 22
not ex w st w in X & w in Y;
end;
definition
let X,Y be integer-membered set;
redefine pred X misses Y means
:: MEMBERED:def 23
not ex i st i in X & i in Y;
end;
definition
let X,Y be natural-membered set;
redefine pred X misses Y means
:: MEMBERED:def 24
not ex n st n in X & n in Y;
end;
theorem :: MEMBERED:25
(for X st X in F holds X is complex-membered) implies union F is
complex-membered;
theorem :: MEMBERED:26
(for X st X in F holds X is ext-real-membered) implies union F is
ext-real-membered;
theorem :: MEMBERED:27
(for X st X in F holds X is real-membered) implies union F is real-membered;
theorem :: MEMBERED:28
(for X st X in F holds X is rational-membered) implies union F is
rational-membered;
theorem :: MEMBERED:29
(for X st X in F holds X is integer-membered) implies union F is
integer-membered;
theorem :: MEMBERED:30
(for X st X in F holds X is natural-membered) implies union F is
natural-membered;
theorem :: MEMBERED:31
for X st X in F & X is complex-membered holds meet F is
complex-membered;
theorem :: MEMBERED:32
for X st X in F & X is ext-real-membered holds meet F is
ext-real-membered;
theorem :: MEMBERED:33
for X st X in F & X is real-membered holds meet F is real-membered;
theorem :: MEMBERED:34
for X st X in F & X is rational-membered holds meet F is
rational-membered;
theorem :: MEMBERED:35
for X st X in F & X is integer-membered holds meet F is
integer-membered;
theorem :: MEMBERED:36
for X st X in F & X is natural-membered holds meet F is
natural-membered;
scheme :: MEMBERED:sch 1
CMSeparation {P[object]}:
ex X being complex-membered set st for c holds c in X
iff P[c];
scheme :: MEMBERED:sch 2
EMSeparation {P[object]}:
ex X being ext-real-membered set st for e holds e in
X iff P[e];
scheme :: MEMBERED:sch 3
RMSeparation {P[object]}:
ex X being real-membered set st for r holds r in X
iff P[r];
scheme :: MEMBERED:sch 4
WMSeparation {P[object]}:
ex X being rational-membered set st for w holds w in
X iff P[w];
scheme :: MEMBERED:sch 5
IMSeparation {P[object]}:
ex X being integer-membered set st for i holds i in X
iff P[i];
scheme :: MEMBERED:sch 6
NMSeparation {P[object]}:
ex X being natural-membered set st for n holds n in X
iff P[n];
registration
cluster non empty natural-membered for set;
end;
:: From REAL_2, AG, 19.12.2008
reserve a,b,d for Real;
theorem :: MEMBERED:37
for X,Y being real-membered set st X<>{} & Y<>{} & for a,b st a in X &
b in Y holds a<=b holds ex d st (for a st a in X holds a<=d) & for b st b in Y
holds d<=b;
:: Added, AK, 2010.04.23
definition
let X be set;
attr X is add-closed means
:: MEMBERED:def 25
for x, y being Complex st x in X & y in X holds x+y in X;
end;
registration
cluster empty -> add-closed for set;
cluster COMPLEX -> add-closed;
cluster REAL -> add-closed;
cluster RAT -> add-closed;
cluster INT -> add-closed;
cluster NAT -> add-closed;
cluster non empty add-closed natural-membered for set;
end;