The abstract of the Mizar article:

Infimum and Supremum of the Set of Real Numbers. Measure Theory

by

Jozef Bialas

Received September 27, 1990

MML identifier: SUPINF_1

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, ARYTM_3, SEQ_2, ARYTM, LATTICES, ORDINAL2, TARSKI, SUPINF_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0,
      REAL_1;
 constructors REAL_1, XREAL_0, MEMBERED, XBOOLE_0;
 clusters XREAL_0, SUBSET_1, XBOOLE_0, MEMBERED, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin

::
:: -infty , +infty and ExtREAL enlarged set of real numbers
::

definition
   func +infty -> set equals
:: SUPINF_1:def 1
 REAL;
end;

canceled;

theorem :: SUPINF_1:2
   not +infty in REAL;

definition let IT be set;
  attr IT is +Inf-like means
:: SUPINF_1:def 2
IT = +infty;
end;

definition
  cluster +Inf-like set;
end;

definition
   mode +Inf is +Inf-like set;
end;

canceled;

theorem :: SUPINF_1:4
     +infty is +Inf;

definition
   func -infty -> set equals
:: SUPINF_1:def 3
 {REAL};
end;

canceled;

theorem :: SUPINF_1:6
   not -infty in REAL;

definition let IT be set;
   attr IT is -Inf-like means
:: SUPINF_1:def 4
IT = -infty;
end;

definition
   cluster -Inf-like set;
end;

definition
   mode -Inf is -Inf-like set;
end;

canceled;

theorem :: SUPINF_1:8
     -infty is -Inf;

definition let IT be set;
   attr IT is ext-real means
:: SUPINF_1:def 5
 IT in REAL \/ {-infty,+infty};
end;

definition
   cluster ext-real set;
end;

definition
   func ExtREAL -> set equals
:: SUPINF_1:def 6
 REAL \/ {-infty,+infty};
end;

definition
  cluster -> ext-real Element of ExtREAL;
end;

definition
   mode R_eal is Element of ExtREAL;
end;

definition
  cluster -> ext-real Real;
end;

canceled;

theorem :: SUPINF_1:10
     for x being Real holds x is R_eal;

theorem :: SUPINF_1:11
   for x being set holds
   x = -infty or x = +infty implies x is R_eal;

definition
   redefine func +infty -> R_eal;
   redefine func -infty -> R_eal;
end;

canceled 2;

theorem :: SUPINF_1:14
   -infty <> +infty;

definition
   let x,y be R_eal;
   pred x <=' y means
:: SUPINF_1:def 7
 ex p,q being Real st p = x & q = y & p <= q if x in REAL & y in REAL
    otherwise x = -infty or y = +infty;
  reflexivity;
  connectedness;
  antonym y <' x;
end;

canceled;

theorem :: SUPINF_1:16
     for x,y being R_eal holds
   ((x is Real & y is Real) implies
   (x <=' y iff ex p,q being Real st (p = x & q = y & p <= q)));

theorem :: SUPINF_1:17
   for x being R_eal holds (x in REAL implies not (x <=' -infty));

theorem :: SUPINF_1:18
   for x being R_eal holds x in REAL implies not +infty <=' x;

theorem :: SUPINF_1:19
     not +infty <=' -infty;

theorem :: SUPINF_1:20
     for x being R_eal holds x <=' +infty;

theorem :: SUPINF_1:21
     for x being R_eal holds -infty <=' x;

theorem :: SUPINF_1:22
   for x,y being R_eal holds x <=' y & y <=' x implies x = y;

theorem :: SUPINF_1:23
     for x being R_eal holds
   x <=' -infty implies x = -infty;

theorem :: SUPINF_1:24
   for x being R_eal holds
   +infty <=' x implies x = +infty;

scheme SepR_eal { P[R_eal]}:
   ex X being Subset of REAL \/ {-infty,+infty} st
   for x being R_eal holds x in X iff P[x];

canceled;

theorem :: SUPINF_1:26
     ExtREAL is non empty set;

theorem :: SUPINF_1:27
     for x being set holds
   x is R_eal iff x in ExtREAL;

canceled;

theorem :: SUPINF_1:29
   for x,y,z being R_eal holds ((x <=' y & y <=' z) implies x <=' z);

definition
   cluster ExtREAL -> non empty;
end;

canceled;

theorem :: SUPINF_1:31
     for x being R_eal holds
   x in REAL implies -infty <' x & x <' +infty;

::
::       Majorant and minorant element of X being SUBDOMAIN of ExtREAL
::

definition
   let X be non empty Subset of ExtREAL;
 canceled;

   mode majorant of X -> R_eal means
:: SUPINF_1:def 9
for x be R_eal holds x in X implies x <=' it;
end;

canceled;

theorem :: SUPINF_1:33
   for X being non empty Subset of ExtREAL holds
   +infty is majorant of X;

theorem :: SUPINF_1:34
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies
   (for UB being R_eal holds UB is majorant of Y implies UB is majorant of X);

definition
   let X be non empty Subset of ExtREAL;
   mode minorant of X -> R_eal means
:: SUPINF_1:def 10
for x be R_eal holds x in X implies it <=' x;
end;

canceled;

theorem :: SUPINF_1:36
   for X being non empty Subset of ExtREAL holds
   -infty is minorant of X;

canceled 2;

theorem :: SUPINF_1:39
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies
   (for LB being R_eal holds LB is minorant of Y implies LB is minorant of X);

definition
   redefine func REAL -> non empty Subset of ExtREAL;
end;

canceled;

theorem :: SUPINF_1:41
     +infty is majorant of REAL;

theorem :: SUPINF_1:42
     -infty is minorant of REAL;

::
::       Bounded above, bounded below and bounded sets of r_eal numbers
::

definition
   let X be non empty Subset of ExtREAL;
   attr X is bounded_above means
:: SUPINF_1:def 11
 ex UB being majorant of X st UB in REAL;
end;

canceled;

theorem :: SUPINF_1:44
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies (Y is bounded_above implies X is bounded_above);

theorem :: SUPINF_1:45
     not REAL is bounded_above;

definition
   let X be non empty Subset of ExtREAL;
   attr X is bounded_below means
:: SUPINF_1:def 12
 ex LB being minorant of X st LB in REAL;
end;

canceled;

theorem :: SUPINF_1:47
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies (Y is bounded_below implies X is bounded_below);

theorem :: SUPINF_1:48
     not REAL is bounded_below;

definition
   let X be non empty Subset of ExtREAL;
   attr X is bounded means
:: SUPINF_1:def 13
X is bounded_above bounded_below;
end;

canceled;

theorem :: SUPINF_1:50
     for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies (Y is bounded implies X is bounded);

theorem :: SUPINF_1:51
   for X being non empty Subset of ExtREAL holds
   ex Y being non empty Subset of ExtREAL st
   for x being R_eal holds x in Y iff x is majorant of X;

::
::       Set of majorant and set of minorant of X being SUBDOMAIN of ExtREAL
::

definition
   let X be non empty Subset of ExtREAL;
   func SetMajorant(X) -> Subset of ExtREAL means
:: SUPINF_1:def 14
 for x being R_eal holds x in it iff x is majorant of X;
end;

definition
   let X be non empty Subset of ExtREAL;
   cluster SetMajorant(X) -> non empty;
end;

canceled 2;

theorem :: SUPINF_1:54
     for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies
   for x being R_eal holds (x in SetMajorant(Y) implies x in SetMajorant(X));

theorem :: SUPINF_1:55
   for X being non empty Subset of ExtREAL holds
   ex Y being non empty Subset of ExtREAL st
   for x being R_eal holds x in Y iff x is minorant of X;

definition
   let X be non empty Subset of ExtREAL;
   func SetMinorant(X) -> Subset of ExtREAL means
:: SUPINF_1:def 15
 for x being R_eal holds x in it iff x is minorant of X;
end;

definition
   let X be non empty Subset of ExtREAL;
   cluster SetMinorant(X) -> non empty;
end;

canceled 2;

theorem :: SUPINF_1:58
     for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies
   for x being R_eal holds (x in SetMinorant(Y) implies x in SetMinorant(X));

theorem :: SUPINF_1:59
   for X being non empty Subset of ExtREAL holds
   X is bounded_above & not X = {-infty} implies
   ex x being Real st x in X & not x = -infty;

theorem :: SUPINF_1:60
   for X being non empty Subset of ExtREAL holds
   X is bounded_below & not X = {+infty} implies
   ex x being Real st x in X & not x = +infty;

canceled;

theorem :: SUPINF_1:62
   for X being non empty Subset of ExtREAL holds
   (X is bounded_above & not X = {-infty}) implies
   ex UB being R_eal st ((UB is majorant of X) &
   (for y being R_eal holds
   (y is majorant of X ) implies (UB <=' y)));

theorem :: SUPINF_1:63
   for X being non empty Subset of ExtREAL holds
   (X is bounded_below & not X = {+infty}) implies
   ex LB being R_eal st ((LB is minorant of X) &
   (for y being R_eal holds
   (y is minorant of X ) implies (y <=' LB)));

theorem :: SUPINF_1:64
   for X being non empty Subset of ExtREAL holds
   X = {-infty} implies X is bounded_above;

theorem :: SUPINF_1:65
   for X being non empty Subset of ExtREAL holds
   X = {+infty} implies X is bounded_below;

theorem :: SUPINF_1:66
   for X being non empty Subset of ExtREAL holds
   X = {-infty} implies
   ex UB being R_eal st ((UB is majorant of X) &
   (for y being R_eal holds
   (y is majorant of X ) implies (UB <=' y)));

theorem :: SUPINF_1:67
   for X being non empty Subset of ExtREAL holds
   X = {+infty} implies
   ex LB being R_eal st ((LB is minorant of X) &
   (for y being R_eal holds
   (y is minorant of X ) implies (y <=' LB)));

theorem :: SUPINF_1:68
   for X being non empty Subset of ExtREAL holds
   X is bounded_above implies
   ex UB being R_eal st ((UB is majorant of X) &
   (for y being R_eal holds
   y is majorant of X implies UB <=' y));

theorem :: SUPINF_1:69
   for X being non empty Subset of ExtREAL holds
   X is bounded_below implies
   ex LB being R_eal st ((LB is minorant of X) &
   (for y being R_eal holds
   (y is minorant of X ) implies (y <=' LB)));

theorem :: SUPINF_1:70
   for X being non empty Subset of ExtREAL holds
   not X is bounded_above implies
   (for y being R_eal holds
   (y is majorant of X implies y = +infty));

theorem :: SUPINF_1:71
   for X being non empty Subset of ExtREAL holds
   not X is bounded_below implies
   (for y being R_eal holds
   (y is minorant of X implies y = -infty));

theorem :: SUPINF_1:72
   for X being non empty Subset of ExtREAL holds
   ex UB being R_eal st ((UB is majorant of X) &
   (for y being R_eal holds
   (y is majorant of X ) implies (UB <=' y)));

theorem :: SUPINF_1:73
   for X being non empty Subset of ExtREAL holds
   ex LB being R_eal st ((LB is minorant of X) &
   (for y being R_eal holds
   (y is minorant of X) implies (y <=' LB)));

::
::       sup X, inf X least upper bound and greatest lower bound of set X
::

definition
   let X be non empty Subset of ExtREAL;
   func sup X -> R_eal means
:: SUPINF_1:def 16
 it is majorant of X &
      for y being R_eal holds
      y is majorant of X implies it <=' y;
end;

canceled 2;

theorem :: SUPINF_1:76
   for X being non empty Subset of ExtREAL holds
   for x being R_eal holds
   x in X implies x <=' sup X;

definition
   let X be non empty Subset of ExtREAL;
   func inf X -> R_eal means
:: SUPINF_1:def 17
 it is minorant of X &
      for y being R_eal holds
      y is minorant of X implies y <=' it;
end;

canceled 2;

theorem :: SUPINF_1:79
   for X being non empty Subset of ExtREAL holds
   for x being R_eal holds
   x in X implies inf X <=' x;

theorem :: SUPINF_1:80
   for X being non empty Subset of ExtREAL holds
   for x being majorant of X holds
   x in X implies x = sup X;

theorem :: SUPINF_1:81
   for X being non empty Subset of ExtREAL holds
   for x being minorant of X holds
   x in X implies x = inf X;

theorem :: SUPINF_1:82
     for X being non empty Subset of ExtREAL holds
   sup X = inf SetMajorant(X) & inf X = sup SetMinorant(X);

theorem :: SUPINF_1:83
     for X being non empty Subset of ExtREAL holds
   X is bounded_above & not X = {-infty} implies sup X in REAL;

theorem :: SUPINF_1:84
     for X being non empty Subset of ExtREAL holds
   X is bounded_below & not X = {+infty} implies inf X in REAL;

definition let x be R_eal;
  redefine func {x} -> Subset of ExtREAL;
end;

definition let x,y be R_eal;
  redefine func {x,y} -> Subset of ExtREAL;
end;

theorem :: SUPINF_1:85
   for x being R_eal holds sup{x} = x;

theorem :: SUPINF_1:86
   for x being R_eal holds inf{x} = x;

theorem :: SUPINF_1:87
     sup {-infty} = -infty;

theorem :: SUPINF_1:88
     sup {+infty} = +infty;

theorem :: SUPINF_1:89
     inf {-infty} = -infty;

theorem :: SUPINF_1:90
     inf {+infty} = +infty;

theorem :: SUPINF_1:91
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies sup X <=' sup Y;

theorem :: SUPINF_1:92
   for x,y being R_eal holds
   for a being R_eal holds
   (x <=' a & y <=' a implies sup{x,y} <=' a);

theorem :: SUPINF_1:93
     for x,y being R_eal holds
   (x <=' y implies sup{x,y} = y) & (y <=' x implies sup{x,y} = x);

theorem :: SUPINF_1:94
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies inf Y <=' inf X;

theorem :: SUPINF_1:95
   for x,y being R_eal holds
   for a being R_eal holds
   (a <=' x & a <=' y implies a <=' inf{x,y});

theorem :: SUPINF_1:96
     for x,y being R_eal holds
   (x <=' y implies inf{x,y} = x) & (y <=' x implies inf{x,y} = y);

theorem :: SUPINF_1:97
   for X being non empty Subset of ExtREAL holds
   for x being R_eal holds
   ((ex y being R_eal st (y in X & x <=' y)) implies x <=' sup X);

theorem :: SUPINF_1:98
   for X being non empty Subset of ExtREAL holds
   for x being R_eal holds
   ((ex y being R_eal st (y in X & y <=' x)) implies inf X <=' x);

theorem :: SUPINF_1:99
     for X,Y being non empty Subset of ExtREAL holds
   (for x being R_eal st x in X holds
   (ex y being R_eal st y in Y & x <=' y)) implies
   sup X <=' sup Y;

theorem :: SUPINF_1:100
     for X,Y being non empty Subset of ExtREAL holds
   (for y being R_eal st y in Y holds
   (ex x being R_eal st x in X & x <=' y)) implies
   inf X <=' inf Y;

theorem :: SUPINF_1:101
   for X,Y being non empty Subset of ExtREAL holds
   for UB1 being majorant of X holds
   for UB2 being majorant of Y holds
   sup{UB1,UB2} is majorant of X \/ Y;

theorem :: SUPINF_1:102
   for X,Y being non empty Subset of ExtREAL holds
   for LB1 being minorant of X holds
   for LB2 being minorant of Y holds
   inf{LB1,LB2} is minorant of X \/ Y;

theorem :: SUPINF_1:103
   for X,Y,S being non empty Subset of ExtREAL holds
   for UB1 being majorant of X holds
   for UB2 being majorant of Y holds
   S = X /\ Y implies inf{UB1,UB2} is majorant of S;

theorem :: SUPINF_1:104
   for X,Y,S being non empty Subset of ExtREAL holds
   for LB1 being minorant of X holds
   for LB2 being minorant of Y holds
   S = X /\ Y implies sup{LB1,LB2} is minorant of S;

theorem :: SUPINF_1:105
     for X,Y being non empty Subset of ExtREAL holds
   sup(X \/ Y) = sup{sup X,sup Y};

theorem :: SUPINF_1:106
     for X,Y being non empty Subset of ExtREAL holds
   inf(X \/ Y) = inf{inf X,inf Y};

theorem :: SUPINF_1:107
     for X,Y,S being non empty Subset of ExtREAL holds
   S = X /\ Y implies sup(S) <=' inf{sup X,sup Y};

theorem :: SUPINF_1:108
     for X,Y,S being non empty Subset of ExtREAL holds
   S = X /\ Y implies sup{inf X,inf Y} <=' inf(S);

definition
   let X be non empty set;
   mode bool_DOMAIN of X -> set means
:: SUPINF_1:def 18
 it is non empty Subset of bool X &
        for A being set holds
        A in it implies A is non empty set;
end;

definition
   let F be bool_DOMAIN of ExtREAL;
   func SUP(F) -> Subset of ExtREAL means
:: SUPINF_1:def 19
for a being R_eal holds
         a in it iff ex A being non empty Subset of ExtREAL st
          A in F & a = sup A;
end;

definition
   let F be bool_DOMAIN of ExtREAL;
   cluster SUP(F) -> non empty;
end;

canceled 3;

theorem :: SUPINF_1:112
   for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies sup S is majorant of SUP(F);

theorem :: SUPINF_1:113
   for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies sup SUP(F) is majorant of S;

theorem :: SUPINF_1:114
     for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies sup S = sup SUP(F);

definition
   let F be bool_DOMAIN of ExtREAL;
   func INF(F) -> Subset of ExtREAL means
:: SUPINF_1:def 20
for a being R_eal holds
        a in it iff ex A being non empty Subset of ExtREAL st A in
 F & a = inf A;
end;

definition
   let F be bool_DOMAIN of ExtREAL;
   cluster INF(F) -> non empty;
end;

canceled 2;

theorem :: SUPINF_1:117
   for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies inf S is minorant of INF(F);

theorem :: SUPINF_1:118
   for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies inf INF(F) is minorant of S;

theorem :: SUPINF_1:119
     for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies inf S = inf INF(F);