Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### 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