:: On the Sets Inhabited by Numbers
::  by Andrzej Trybulec
::
:: Received August 23, 2003
:: Copyright (c) 2003-2021 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;