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