Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### On the Sets Inhabited by Numbers

by
Andrzej Trybulec

Received August 23, 2003

MML identifier: MEMBERED
[ Mizar article, MML identifier index ]

```environ

vocabulary MEMBERED, XCMPLX_0, ARYTM, INT_1, ORDINAL2, BOOLE, COMPLEX1, RAT_1,
ORDINAL1, TARSKI, SETFAM_1;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, NUMBERS, XCMPLX_0,
XREAL_0, RAT_1, INT_1, ORDINAL1, ORDINAL2;
constructors XCMPLX_0, RAT_1, ENUMSET1, SETFAM_1;
clusters INT_1, NUMBERS, ARYTM_3, XREAL_0, RAT_1, XBOOLE_0;
requirements NUMERALS, BOOLE, SUBSET;

begin

reserve x, 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 real-membered means
:: MEMBERED:def 2
x in X implies x is real;
attr X is rational-membered means
:: MEMBERED:def 3
x in X implies x is rational;
attr X is integer-membered means
:: MEMBERED:def 4
x in X implies x is integer;
attr X is natural-membered means
:: MEMBERED:def 5
x in X implies x is natural;
end;

definition
cluster natural-membered -> integer-membered set;
cluster integer-membered -> rational-membered set;
cluster rational-membered -> real-membered set;
cluster real-membered -> complex-membered set;
end;

definition
cluster non empty natural-membered set;
end;

definition
cluster -> complex-membered Subset of COMPLEX;
cluster -> real-membered Subset of REAL;
cluster -> rational-membered Subset of RAT;
cluster -> integer-membered Subset of INT;
cluster -> natural-membered Subset of NAT;
end;

definition
cluster COMPLEX -> complex-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 real-membered implies X c= REAL;

theorem :: MEMBERED:3
X is rational-membered implies X c= RAT;

theorem :: MEMBERED:4
X is integer-membered implies X c= INT;

theorem :: MEMBERED:5
X is natural-membered implies X c= NAT;

definition let X be complex-membered set;
cluster -> complex Element of X;
end;

definition let X be real-membered set;
cluster -> real Element of X;
end;

definition let X be rational-membered set;
cluster -> rational Element of X;
end;

definition let X be integer-membered set;
cluster -> integer Element of X;
end;

definition let X be natural-membered set;
cluster -> natural Element of X;
end;

reserve c, c1, c2, c3 for complex number,
r, r1, r2, r3 for real number,
w, w1, w2, w3 for rational number,
i, i1, i2, i3 for integer number,
n, n1, n2, n3 for natural number;

theorem :: MEMBERED:6
for X being non empty complex-membered set
ex c st c in X;

theorem :: MEMBERED:7
for X being non empty real-membered set
ex r st r in X;

theorem :: MEMBERED:8
for X being non empty rational-membered set
ex w st w in X;

theorem :: MEMBERED:9
for X being non empty integer-membered set
ex i st i in X;

theorem :: MEMBERED:10
for X being non empty natural-membered set
ex n st n in X;

theorem :: MEMBERED:11
for X being complex-membered set
st for c holds c in X
holds X = COMPLEX;

theorem :: MEMBERED:12
for X being real-membered set
st for r holds r in X
holds X = REAL;

theorem :: MEMBERED:13
for X being rational-membered set
st for w holds w in X
holds X = RAT;

theorem :: MEMBERED:14
for X being integer-membered set
st for i holds i in X
holds X = INT;

theorem :: MEMBERED:15
for X being natural-membered set
st for n holds n in X
holds X = NAT;

theorem :: MEMBERED:16
for Y being complex-membered set st X c= Y
holds X is complex-membered;

theorem :: MEMBERED:17
for Y being real-membered set st X c= Y
holds X is real-membered;

theorem :: MEMBERED:18
for Y being rational-membered set st X c= Y
holds X is rational-membered;

theorem :: MEMBERED:19
for Y being integer-membered set st X c= Y
holds X is integer-membered;

theorem :: MEMBERED:20
for Y being natural-membered set st X c= Y
holds X is natural-membered;

definition
cluster {} -> natural-membered;
end;

definition
cluster empty -> natural-membered set;
end;

definition let c;
cluster {c} -> complex-membered;
end;

definition let r;
cluster {r} -> real-membered;
end;

definition let w;
cluster {w} -> rational-membered;
end;

definition let i;
cluster {i} -> integer-membered;
end;

definition let n;
cluster {n} -> natural-membered;
end;

definition let c1,c2;
cluster {c1,c2} -> complex-membered;
end;

definition let r1,r2;
cluster {r1,r2} -> real-membered;
end;

definition let w1,w2;
cluster {w1,w2} -> rational-membered;
end;

definition let i1,i2;
cluster {i1,i2} -> integer-membered;
end;

definition let n1,n2;
cluster {n1,n2} -> natural-membered;
end;

definition let c1,c2,c3;
cluster {c1,c2,c3} -> complex-membered;
end;

definition let r1,r2,r3;
cluster {r1,r2,r3} -> real-membered;
end;

definition let w1,w2,w3;
cluster {w1,w2,w3} -> rational-membered;
end;

definition let i1,i2,i3;
cluster {i1,i2,i3} -> integer-membered;
end;

definition let n1,n2,n3;
cluster {n1,n2,n3} -> natural-membered;
end;

definition let X be complex-membered set;
cluster -> complex-membered Subset of X;
end;

definition let X be real-membered set;
cluster -> real-membered Subset of X;
end;

definition let X be rational-membered set;
cluster -> rational-membered Subset of X;
end;

definition let X be integer-membered set;
cluster -> integer-membered Subset of X;
end;

definition let X be natural-membered set;
cluster -> natural-membered Subset of X;
end;

definition let X,Y be complex-membered set;
cluster X \/ Y -> complex-membered;
end;

definition let X,Y be real-membered set;
cluster X \/ Y -> real-membered;
end;

definition let X,Y be rational-membered set;
cluster X \/ Y -> rational-membered;
end;

definition let X,Y be integer-membered set;
cluster X \/ Y -> integer-membered;
end;

definition let X,Y be natural-membered set;
cluster X \/ Y -> natural-membered;
end;

definition let X be complex-membered set, Y be set;
cluster X /\ Y -> complex-membered;
cluster Y /\ X -> complex-membered;
end;

definition let X be real-membered set, Y be set;
cluster X /\ Y -> real-membered;
cluster Y /\ X -> real-membered;
end;

definition let X be rational-membered set, Y be set;
cluster X /\ Y -> rational-membered;
cluster Y /\ X -> rational-membered;
end;

definition let X be integer-membered set, Y be set;
cluster X /\ Y -> integer-membered;
cluster Y /\ X -> integer-membered;
end;

definition let X be natural-membered set, Y be set;
cluster X /\ Y -> natural-membered;
cluster Y /\ X -> natural-membered;
end;

definition let X be complex-membered set, Y be set;
cluster X \ Y -> complex-membered;
end;

definition let X be real-membered set, Y be set;
cluster X \ Y -> real-membered;
end;

definition let X be rational-membered set, Y be set;
cluster X \ Y -> rational-membered;
end;

definition let X be integer-membered set, Y be set;
cluster X \ Y -> integer-membered;
end;

definition let X be natural-membered set, Y be set;
cluster X \ Y -> natural-membered;
end;

definition let X,Y be complex-membered set;
cluster X \+\ Y -> complex-membered;
end;

definition let X,Y be real-membered set;
cluster X \+\ Y -> real-membered;
end;

definition let X,Y be rational-membered set;
cluster X \+\ Y -> rational-membered;
end;

definition let X,Y be integer-membered set;
cluster X \+\ Y -> integer-membered;
end;

definition let X,Y be natural-membered set;
cluster X \+\ Y -> natural-membered;
end;

definition let X,Y be complex-membered set;
redefine pred X c= Y means
:: MEMBERED:def 6
c in X implies c in Y;
end;

definition let X,Y be real-membered set;
redefine pred X c= Y means
:: MEMBERED:def 7
r in X implies r in Y;
end;

definition let X,Y be rational-membered set;
redefine pred X c= Y means
:: MEMBERED:def 8
w in X implies w in Y;
end;

definition let X,Y be integer-membered set;
redefine pred X c= Y means
:: MEMBERED:def 9
i in X implies i in Y;
end;

definition let X,Y be natural-membered set;
redefine pred X c= Y means
:: MEMBERED:def 10
n in X implies n in Y;
end;

definition let X,Y be complex-membered set;
redefine pred X = Y means
:: MEMBERED:def 11
c in X iff c in Y;
end;

definition let X,Y be real-membered set;
redefine pred X = Y means
:: MEMBERED:def 12
r in X iff r in Y;
end;

definition let X,Y be rational-membered set;
redefine pred X = Y means
:: MEMBERED:def 13
w in X iff w in Y;
end;

definition let X,Y be integer-membered set;
redefine pred X = Y means
:: MEMBERED:def 14
i in X iff i in Y;
end;

definition let X,Y be natural-membered set;
redefine pred X = Y means
:: MEMBERED:def 15
n in X iff n in Y;
end;

definition let X,Y be complex-membered set;
redefine pred X meets Y means
:: MEMBERED:def 16
ex c st c in X & c in Y;
end;

definition let X,Y be real-membered set;
redefine pred X meets Y means
:: MEMBERED:def 17
ex r st r in X & r in Y;
end;

definition let X,Y be rational-membered set;
redefine pred X meets Y means
:: MEMBERED:def 18
ex w st w in X & w in Y;
end;

definition let X,Y be integer-membered set;
redefine pred X meets Y means
:: MEMBERED:def 19
ex i st i in X & i in Y;
end;

definition let X,Y be natural-membered set;
redefine pred X meets Y means
:: MEMBERED:def 20
ex n st n in X & n in Y;
end;

theorem :: MEMBERED:21
(for X st X in F holds X is complex-membered)
implies union F is complex-membered;

theorem :: MEMBERED:22
(for X st X in F holds X is real-membered)
implies union F is real-membered;

theorem :: MEMBERED:23
(for X st X in F holds X is rational-membered)
implies union F is rational-membered;

theorem :: MEMBERED:24
(for X st X in F holds X is integer-membered)
implies union F is integer-membered;

theorem :: MEMBERED:25
(for X st X in F holds X is natural-membered)
implies union F is natural-membered;

theorem :: MEMBERED:26
for X st X in F & X is complex-membered
holds meet F is complex-membered;

theorem :: MEMBERED:27
for X st X in F & X is real-membered
holds meet F is real-membered;

theorem :: MEMBERED:28
for X st X in F & X is rational-membered
holds meet F is rational-membered;

theorem :: MEMBERED:29
for X st X in F & X is integer-membered
holds meet F is integer-membered;

theorem :: MEMBERED:30
for X st X in F & X is natural-membered
holds meet F is natural-membered;

scheme CM_Separation {P[set]}:
ex X being complex-membered set st
for c holds c in X iff P[c];

scheme RM_Separation {P[set]}:
ex X being real-membered set st
for r holds r in X iff P[r];

scheme WM_Separation {P[set]}:
ex X being rational-membered set st
for w holds w in X iff P[w];

scheme IM_Separation {P[set]}:
ex X being integer-membered set st
for i holds i in X iff P[i];

scheme NM_Separation {P[set]}:
ex X being natural-membered set st
for n holds n in X iff P[n];
```

Back to top