:: On the Sets Inhabited by Numbers
:: by Andrzej Trybulec
::
:: Received August 23, 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 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;
definitions XCMPLX_0, XREAL_0, INT_1, TARSKI, RAT_1, XBOOLE_0, XXREAL_0;
equalities XBOOLE_0;
expansions XCMPLX_0, XREAL_0, INT_1, TARSKI, RAT_1, XBOOLE_0, XXREAL_0;
theorems INT_1, XBOOLE_0, XREAL_0, XCMPLX_0, RAT_1, SUBSET_1, ORDINAL1,
TARSKI, ENUMSET1, XBOOLE_1, SETFAM_1, NUMBERS, XXREAL_0, AXIOMS;
schemes XBOOLE_0;
begin
reserve x for object, X, F for set;
definition
let X be set;
attr X is complex-membered means
:Def1:
x in X implies x is complex;
attr X is ext-real-membered means
:Def2:
x in X implies x is ext-real;
attr X is real-membered means
:Def3:
x in X implies x is real;
attr X is rational-membered means
:Def4:
x in X implies x is rational;
attr X is integer-membered means
:Def5:
x in X implies x is integer;
attr X is natural-membered means
:Def6:
x in X implies x is natural;
end;
registration
cluster natural-membered -> integer-membered for set;
coherence
proof
let X;
assume
A1: X is natural-membered;
let x;
assume x in X;
then x is natural by A1;
then x in omega by ORDINAL1:def 12;
hence x in INT by NUMBERS:17;
end;
cluster integer-membered -> rational-membered for set;
coherence
proof
let X;
assume
A2: X is integer-membered;
let x;
assume x in X;
then x is integer by A2;
then x in INT;
hence x in RAT by NUMBERS:14;
end;
cluster rational-membered -> real-membered for set;
coherence
proof
let X;
assume
A3: X is rational-membered;
let x;
assume x in X;
then x is rational by A3;
then x in RAT;
hence x in REAL by NUMBERS:12;
end;
cluster real-membered -> ext-real-membered for set;
coherence
proof
let X;
assume
A4: X is real-membered;
let x;
assume x in X;
then x is real by A4;
then x in REAL;
hence x in ExtREAL by NUMBERS:31;
end;
cluster real-membered -> complex-membered for set;
coherence
proof
let X;
assume
A5: X is real-membered;
let x;
assume x in X;
then x is real by A5;
then x in REAL;
hence x in COMPLEX by NUMBERS:11;
end;
end;
registration
cluster non empty natural-membered for set;
existence
proof
take {0};
thus {0} is non empty;
let x;
assume x in {0};
hence thesis by TARSKI:def 1;
end;
end;
registration
cluster COMPLEX -> complex-membered;
coherence;
cluster ExtREAL -> ext-real-membered;
coherence
proof
let x;
thus thesis;
end;
cluster REAL -> real-membered;
coherence;
cluster RAT -> rational-membered;
coherence
proof
let x;
thus thesis;
end;
cluster INT -> integer-membered;
coherence;
cluster NAT -> natural-membered;
coherence;
end;
theorem Th1:
X is complex-membered implies X c= COMPLEX
proof
assume
A1: X is complex-membered;
let x be object;
assume x in X;
then x is complex by A1;
hence thesis;
end;
theorem Th2:
X is ext-real-membered implies X c= ExtREAL
proof
assume
A1: X is ext-real-membered;
let x be object;
assume x in X;
then x is ext-real by A1;
hence thesis;
end;
theorem Th3:
X is real-membered implies X c= REAL
proof
assume
A1: X is real-membered;
let x be object;
assume x in X;
then x is real by A1;
hence thesis;
end;
theorem Th4:
X is rational-membered implies X c= RAT
proof
assume
A1: X is rational-membered;
let x be object;
assume x in X;
then x is rational by A1;
hence thesis;
end;
theorem Th5:
X is integer-membered implies X c= INT
proof
assume
A1: X is integer-membered;
let x be object;
assume x in X;
then x is integer by A1;
hence thesis;
end;
theorem Th6:
X is natural-membered implies X c= NAT
by ORDINAL1:def 12;
registration
let X be complex-membered set;
cluster -> complex for Element of X;
coherence
proof
let e be Element of X;
per cases;
suppose
X is empty;
hence thesis by SUBSET_1:def 1;
end;
suppose
X is non empty;
hence thesis by Def1;
end;
end;
end;
registration
let X be ext-real-membered set;
cluster -> ext-real for Element of X;
coherence
proof
let e be Element of X;
per cases;
suppose
X is empty;
hence thesis by SUBSET_1:def 1;
end;
suppose
X is non empty;
hence thesis by Def2;
end;
end;
end;
registration
let X be real-membered set;
cluster -> real for Element of X;
coherence
proof
let e be Element of X;
per cases;
suppose
X is empty;
hence thesis by SUBSET_1:def 1;
end;
suppose
X is non empty;
hence thesis by Def3;
end;
end;
end;
registration
let X be rational-membered set;
cluster -> rational for Element of X;
coherence
proof
let e be Element of X;
per cases;
suppose
X is empty;
hence thesis by SUBSET_1:def 1;
end;
suppose
X is non empty;
hence thesis by Def4;
end;
end;
end;
registration
let X be integer-membered set;
cluster -> integer for Element of X;
coherence
proof
let e be Element of X;
per cases;
suppose
X is empty;
hence thesis by SUBSET_1:def 1;
end;
suppose
X is non empty;
hence thesis by Def5;
end;
end;
end;
registration
let X be natural-membered set;
cluster -> natural for Element of X;
coherence
proof
let e be Element of X;
per cases;
suppose
X is empty;
hence thesis by SUBSET_1:def 1;
end;
suppose
X is non empty;
hence thesis by Def6;
end;
end;
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
for X being non empty complex-membered set ex c st c in X
proof
let X be non empty complex-membered set;
ex x being object st x in X by XBOOLE_0:def 1;
hence thesis;
end;
theorem
for X being non empty ext-real-membered set ex e st e in X
proof
let X be non empty ext-real-membered set;
ex x being object st x in X by XBOOLE_0:def 1;
hence thesis;
end;
theorem
for X being non empty real-membered set ex r st r in X
proof
let X be non empty real-membered set;
ex x being object st x in X by XBOOLE_0:def 1;
hence thesis;
end;
theorem
for X being non empty rational-membered set ex w st w in X
proof
let X be non empty rational-membered set;
ex x being object st x in X by XBOOLE_0:def 1;
hence thesis;
end;
theorem
for X being non empty integer-membered set ex i st i in X
proof
let X be non empty integer-membered set;
ex x being object st x in X by XBOOLE_0:def 1;
hence thesis;
end;
theorem
for X being non empty natural-membered set ex n st n in X
proof
let X be non empty natural-membered set;
ex x being object st x in X by XBOOLE_0:def 1;
hence thesis;
end;
theorem
for X being complex-membered set st for c holds c in X holds X = COMPLEX
proof
let X be complex-membered set such that
A1: for c holds c in X;
thus X c= COMPLEX by Th1;
let e be object;
assume e in COMPLEX;
hence thesis by A1;
end;
theorem
for X being ext-real-membered set st for e holds e in X holds X = ExtREAL
proof
let X be ext-real-membered set such that
A1: for e holds e in X;
thus X c= ExtREAL by Th2;
let e be object;
assume e in ExtREAL;
hence thesis by A1;
end;
theorem
for X being real-membered set st for r holds r in X holds X = REAL
proof
let X be real-membered set such that
A1: for r holds r in X;
thus X c= REAL by Th3;
let e be object;
assume e in REAL;
hence thesis by A1;
end;
theorem
for X being rational-membered set st for w holds w in X holds X = RAT
proof
let X be rational-membered set such that
A1: for w holds w in X;
thus X c= RAT by Th4;
let e be object;
assume e in RAT;
hence thesis by A1;
end;
theorem
for X being integer-membered set st for i holds i in X holds X = INT
proof
let X be integer-membered set such that
A1: for i holds i in X;
thus X c= INT by Th5;
let e be object;
assume e in INT;
hence thesis by A1;
end;
theorem
for X being natural-membered set st for n holds n in X holds X = NAT
proof
let X be natural-membered set such that
A1: for n holds n in X;
thus X c= NAT by Th6;
let e be object;
assume e in NAT;
hence thesis by A1;
end;
theorem Th19:
for Y being complex-membered set st X c= Y holds X is complex-membered;
theorem Th20:
for Y being ext-real-membered set st X c= Y holds X is ext-real-membered;
theorem Th21:
for Y being real-membered set st X c= Y holds X is real-membered;
theorem Th22:
for Y being rational-membered set st X c= Y holds X is rational-membered;
theorem Th23:
for Y being integer-membered set st X c= Y holds X is integer-membered;
theorem Th24:
for Y being natural-membered set st X c= Y holds X is natural-membered;
registration
cluster empty -> natural-membered for set;
coherence;
end;
registration
let c;
cluster {c} -> complex-membered;
coherence
by TARSKI:def 1;
end;
registration
let e be ExtReal;
cluster {e} -> ext-real-membered;
coherence
by TARSKI:def 1;
end;
registration
let r;
cluster {r} -> real-membered;
coherence
by TARSKI:def 1;
end;
registration
let w;
cluster {w} -> rational-membered;
coherence
by TARSKI:def 1;
end;
registration
let i;
cluster {i} -> integer-membered;
coherence
by TARSKI:def 1;
end;
registration
let n;
cluster {n} -> natural-membered;
coherence
by TARSKI:def 1;
end;
registration
let c1,c2;
cluster {c1,c2} -> complex-membered;
coherence
by TARSKI:def 2;
end;
registration
let e1,e2 be ExtReal;
cluster {e1,e2} -> ext-real-membered;
coherence
by TARSKI:def 2;
end;
registration
let r1,r2;
cluster {r1,r2} -> real-membered;
coherence
by TARSKI:def 2;
end;
registration
let w1,w2;
cluster {w1,w2} -> rational-membered;
coherence
by TARSKI:def 2;
end;
registration
let i1,i2;
cluster {i1,i2} -> integer-membered;
coherence
by TARSKI:def 2;
end;
registration
let n1,n2;
cluster {n1,n2} -> natural-membered;
coherence
by TARSKI:def 2;
end;
registration
let c1,c2,c3;
cluster {c1,c2,c3} -> complex-membered;
coherence
by ENUMSET1:def 1;
end;
registration
let e1,e2,e3 be ExtReal;
cluster {e1,e2,e3} -> ext-real-membered;
coherence
by ENUMSET1:def 1;
end;
registration
let r1,r2,r3;
cluster {r1,r2,r3} -> real-membered;
coherence
by ENUMSET1:def 1;
end;
registration
let w1,w2,w3;
cluster {w1,w2,w3} -> rational-membered;
coherence
by ENUMSET1:def 1;
end;
registration
let i1,i2,i3;
cluster {i1,i2,i3} -> integer-membered;
coherence
by ENUMSET1:def 1;
end;
registration
let n1,n2,n3;
cluster {n1,n2,n3} -> natural-membered;
coherence
by ENUMSET1:def 1;
end;
registration
let X be complex-membered set;
cluster -> complex-membered for Subset of X;
coherence;
end;
registration
let X be ext-real-membered set;
cluster -> ext-real-membered for Subset of X;
coherence;
end;
registration
let X be real-membered set;
cluster -> real-membered for Subset of X;
coherence;
end;
registration
let X be rational-membered set;
cluster -> rational-membered for Subset of X;
coherence;
end;
registration
let X be integer-membered set;
cluster -> integer-membered for Subset of X;
coherence;
end;
registration
let X be natural-membered set;
cluster -> natural-membered for Subset of X;
coherence;
end;
registration
let X,Y be complex-membered set;
cluster X \/ Y -> complex-membered;
coherence
proof
let x;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 3;
hence thesis;
end;
end;
registration
let X,Y be ext-real-membered set;
cluster X \/ Y -> ext-real-membered;
coherence
proof
let x;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 3;
hence thesis;
end;
end;
registration
let X,Y be real-membered set;
cluster X \/ Y -> real-membered;
coherence
proof
let x;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 3;
hence thesis;
end;
end;
registration
let X,Y be rational-membered set;
cluster X \/ Y -> rational-membered;
coherence
proof
let x;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 3;
hence thesis;
end;
end;
registration
let X,Y be integer-membered set;
cluster X \/ Y -> integer-membered;
coherence
proof
let x;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 3;
hence thesis;
end;
end;
registration
let X,Y be natural-membered set;
cluster X \/ Y -> natural-membered;
coherence
proof
let x;
assume x in X \/ Y;
then x in X or x in Y by XBOOLE_0:def 3;
hence thesis;
end;
end;
registration
let X be complex-membered set, Y be set;
cluster X /\ Y -> complex-membered;
coherence by Th19,XBOOLE_1:17;
cluster Y /\ X -> complex-membered;
coherence;
end;
registration
let X be ext-real-membered set, Y be set;
cluster X /\ Y -> ext-real-membered;
coherence by Th20,XBOOLE_1:17;
cluster Y /\ X -> ext-real-membered;
coherence;
end;
registration
let X be real-membered set, Y be set;
cluster X /\ Y -> real-membered;
coherence by Th21,XBOOLE_1:17;
cluster Y /\ X -> real-membered;
coherence;
end;
registration
let X be rational-membered set, Y be set;
cluster X /\ Y -> rational-membered;
coherence by Th22,XBOOLE_1:17;
cluster Y /\ X -> rational-membered;
coherence;
end;
registration
let X be integer-membered set, Y be set;
cluster X /\ Y -> integer-membered;
coherence by Th23,XBOOLE_1:17;
cluster Y /\ X -> integer-membered;
coherence;
end;
registration
let X be natural-membered set, Y be set;
cluster X /\ Y -> natural-membered;
coherence by Th24,XBOOLE_1:17;
cluster Y /\ X -> natural-membered;
coherence;
end;
registration
let X be complex-membered set, Y be set;
cluster X \ Y -> complex-membered;
coherence;
end;
registration
let X be ext-real-membered set, Y be set;
cluster X \ Y -> ext-real-membered;
coherence;
end;
registration
let X be real-membered set, Y be set;
cluster X \ Y -> real-membered;
coherence;
end;
registration
let X be rational-membered set, Y be set;
cluster X \ Y -> rational-membered;
coherence;
end;
registration
let X be integer-membered set, Y be set;
cluster X \ Y -> integer-membered;
coherence;
end;
registration
let X be natural-membered set, Y be set;
cluster X \ Y -> natural-membered;
coherence;
end;
registration
let X,Y be complex-membered set;
cluster X \+\ Y -> complex-membered;
coherence;
end;
registration
let X,Y be ext-real-membered set;
cluster X \+\ Y -> ext-real-membered;
coherence;
end;
registration
let X,Y be real-membered set;
cluster X \+\ Y -> real-membered;
coherence;
end;
registration
let X,Y be rational-membered set;
cluster X \+\ Y -> rational-membered;
coherence;
end;
registration
let X,Y be integer-membered set;
cluster X \+\ Y -> integer-membered;
coherence;
end;
registration
let X,Y be natural-membered set;
cluster X \+\ Y -> natural-membered;
coherence;
end;
definition
let X be complex-membered set, Y be set;
redefine pred X c= Y means
c in X implies c in Y;
compatibility;
end;
definition
let X be ext-real-membered set, Y be set;
redefine pred X c= Y means
e in X implies e in Y;
compatibility;
end;
definition
let X be real-membered set, Y be set;
redefine pred X c= Y means
r in X implies r in Y;
compatibility;
end;
definition
let X be rational-membered set, Y be set;
redefine pred X c= Y means
w in X implies w in Y;
compatibility;
end;
definition
let X be integer-membered set, Y be set;
redefine pred X c= Y means
i in X implies i in Y;
compatibility;
end;
definition
let X be natural-membered set, Y be set;
redefine pred X c= Y means
n in X implies n in Y;
compatibility;
end;
definition
let X,Y be complex-membered set;
redefine pred X = Y means
c in X iff c in Y;
compatibility
proof
thus X = Y implies for c holds c in X iff c in Y;
assume c in X iff c in Y;
hence X c= Y & Y c= X;
end;
end;
definition
let X,Y be ext-real-membered set;
redefine pred X = Y means
e in X iff e in Y;
compatibility
proof
thus X = Y implies for e holds e in X iff e in Y;
assume e in X iff e in Y;
then X c= Y & Y c= X;
hence thesis;
end;
end;
definition
let X,Y be real-membered set;
redefine pred X = Y means
r in X iff r in Y;
compatibility;
end;
definition
let X,Y be rational-membered set;
redefine pred X = Y means
w in X iff w in Y;
compatibility;
end;
definition
let X,Y be integer-membered set;
redefine pred X = Y means
i in X iff i in Y;
compatibility;
end;
definition
let X,Y be natural-membered set;
redefine pred X = Y means
n in X iff n in Y;
compatibility;
end;
definition
let X,Y be complex-membered set;
redefine pred X meets Y means
ex c st c in X & c in Y;
compatibility
proof
thus X misses Y implies not ex c st c in X & c in Y by XBOOLE_0:3;
assume
A1: not ex c st c in X & c in Y;
assume X meets Y;
then ex x being object st x in X & x in Y by XBOOLE_0:3;
hence thesis by A1;
end;
end;
definition
let X,Y be ext-real-membered set;
redefine pred X meets Y means
ex e st e in X & e in Y;
compatibility
proof
thus X misses Y implies not ex e st e in X & e in Y by XBOOLE_0:3;
assume
A1: not ex e st e in X & e in Y;
assume X meets Y;
then ex x being object st x in X & x in Y by XBOOLE_0:3;
hence thesis by A1;
end;
end;
definition
let X,Y be real-membered set;
redefine pred X meets Y means
ex r st r in X & r in Y;
compatibility;
end;
definition
let X,Y be rational-membered set;
redefine pred X meets Y means
ex w st w in X & w in Y;
compatibility;
end;
definition
let X,Y be integer-membered set;
redefine pred X meets Y means
ex i st i in X & i in Y;
compatibility;
end;
definition
let X,Y be natural-membered set;
redefine pred X meets Y means
ex n st n in X & n in Y;
compatibility;
end;
theorem
(for X st X in F holds X is complex-membered) implies union F is
complex-membered
proof
assume
A1: for X st X in F holds X is complex-membered;
let x;
assume x in union F;
then consider X such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is complex-membered by A1,A3;
hence thesis by A2;
end;
theorem
(for X st X in F holds X is ext-real-membered) implies union F is
ext-real-membered
proof
assume
A1: for X st X in F holds X is ext-real-membered;
let x;
assume x in union F;
then consider X such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is ext-real-membered by A1,A3;
hence thesis by A2;
end;
theorem
(for X st X in F holds X is real-membered) implies union F is real-membered
proof
assume
A1: for X st X in F holds X is real-membered;
let x;
assume x in union F;
then consider X such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is real-membered by A1,A3;
hence thesis by A2;
end;
theorem
(for X st X in F holds X is rational-membered) implies union F is
rational-membered
proof
assume
A1: for X st X in F holds X is rational-membered;
let x;
assume x in union F;
then consider X such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is rational-membered by A1,A3;
hence thesis by A2;
end;
theorem
(for X st X in F holds X is integer-membered) implies union F is
integer-membered
proof
assume
A1: for X st X in F holds X is integer-membered;
let x;
assume x in union F;
then consider X such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is integer-membered by A1,A3;
hence thesis by A2;
end;
theorem
(for X st X in F holds X is natural-membered) implies union F is
natural-membered
proof
assume
A1: for X st X in F holds X is natural-membered;
let x;
assume x in union F;
then consider X such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is natural-membered by A1,A3;
hence thesis by A2;
end;
theorem
for X st X in F & X is complex-membered holds meet F is
complex-membered by Th19,SETFAM_1:3;
theorem
for X st X in F & X is ext-real-membered holds meet F is
ext-real-membered by Th20,SETFAM_1:3;
theorem
for X st X in F & X is real-membered holds meet F is real-membered by Th21,
SETFAM_1:3;
theorem
for X st X in F & X is rational-membered holds meet F is
rational-membered by Th22,SETFAM_1:3;
theorem
for X st X in F & X is integer-membered holds meet F is
integer-membered by Th23,SETFAM_1:3;
theorem
for X st X in F & X is natural-membered holds meet F is
natural-membered by Th24,SETFAM_1:3;
scheme
CMSeparation {P[object]}:
ex X being complex-membered set st for c holds c in X
iff P[c] proof
consider X being set such that
A1: for x being object holds x in X iff x in COMPLEX & P[x]
from XBOOLE_0:sch 1;
X is complex-membered
proof
let x;
assume x in X;
then x in COMPLEX by A1;
hence thesis;
end;
then reconsider X as complex-membered set;
take X;
let c;
c in COMPLEX by XCMPLX_0:def 2;
hence thesis by A1;
end;
scheme
EMSeparation {P[object]}:
ex X being ext-real-membered set st for e holds e in
X iff P[e] proof
consider X being set such that
A1: for x being object holds x in X iff x in ExtREAL & P[x]
from XBOOLE_0:sch 1;
X is ext-real-membered
proof
let x;
assume x in X;
then x in ExtREAL by A1;
hence thesis;
end;
then reconsider X as ext-real-membered set;
take X;
let e;
e in ExtREAL by XXREAL_0:def 1;
hence thesis by A1;
end;
scheme
RMSeparation {P[object]}:
ex X being real-membered set st for r holds r in X
iff P[r] proof
consider X being set such that
A1: for x being object holds x in X iff x in REAL & P[x]
from XBOOLE_0:sch 1;
X is real-membered
proof
let x;
assume x in X;
then x in REAL by A1;
hence thesis;
end;
then reconsider X as real-membered set;
take X;
let r;
r in REAL by XREAL_0:def 1;
hence thesis by A1;
end;
scheme
WMSeparation {P[object]}:
ex X being rational-membered set st for w holds w in
X iff P[w] proof
consider X being set such that
A1: for x being object holds x in X iff x in RAT & P[x]
from XBOOLE_0:sch 1;
X is rational-membered
proof
let x;
assume x in X;
then x in RAT by A1;
hence thesis;
end;
then reconsider X as rational-membered set;
take X;
let w;
w in RAT by RAT_1:def 2;
hence thesis by A1;
end;
scheme
IMSeparation {P[object]}:
ex X being integer-membered set st for i holds i in X
iff P[i] proof
consider X being set such that
A1: for x being object holds x in X iff x in INT & P[x]
from XBOOLE_0:sch 1;
X is integer-membered
proof
let x;
assume x in X;
then x in INT by A1;
hence thesis;
end;
then reconsider X as integer-membered set;
take X;
let i;
i in INT by INT_1:def 2;
hence thesis by A1;
end;
scheme
NMSeparation {P[object]}:
ex X being natural-membered set st for n holds n in X
iff P[n] proof
consider X being set such that
A1: for x being object holds x in X iff x in NAT & P[x]
from XBOOLE_0:sch 1;
X is natural-membered
proof
let x;
assume x in X;
then x in NAT by A1;
hence thesis;
end;
then reconsider X as natural-membered set;
take X;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
registration
cluster non empty natural-membered for set;
existence
proof
set X = the non empty natural-membered set;
take X;
thus thesis;
end;
end;
:: From REAL_2, AG, 19.12.2008
reserve a,b,d for Real;
theorem
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
proof
let X,Y be real-membered set;
set x = the Element of X;
reconsider a=x as Real;
set y = the Element of Y;
reconsider b=y as Real;
assume X<>{} & Y<>{};
then
A1: a in X & b in Y;
A2: X c= REAL & Y c= REAL by Th3;
assume for a,b st a in X & b in Y holds a<=b;
then consider d being Real such that
A3: for a,b being Real st a in X & b in Y holds a<=d & d<=b by A2,
AXIOMS:1;
reconsider d as Real;
take d;
thus thesis by A1,A3;
end;
:: Added, AK, 2010.04.23
definition
let X be set;
attr X is add-closed means
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;
coherence;
cluster COMPLEX -> add-closed;
coherence
by XCMPLX_0:def 2;
cluster REAL -> add-closed;
coherence
by XREAL_0:def 1;
cluster RAT -> add-closed;
coherence
by RAT_1:def 2;
cluster INT -> add-closed;
coherence
by INT_1:def 2;
cluster NAT -> add-closed;
coherence
by ORDINAL1:def 12;
cluster non empty add-closed natural-membered for set;
existence
proof
take NAT;
thus thesis;
end;
end;