Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

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

by
Jozef Bialas

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);
```