:: Infimum and Supremum of the Set of Real Numbers. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990-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 SUBSET_1, NUMBERS, XXREAL_0, MEMBERED, XXREAL_2, ORDINAL1,
XBOOLE_0, TARSKI, ORDINAL2, SETFAM_1, ZFMISC_1, SUPINF_1;
notations XBOOLE_0, SUBSET_1, ZFMISC_1, SETFAM_1, DOMAIN_1, ORDINAL1, NUMBERS,
MEMBERED, XXREAL_0, XXREAL_2;
constructors NUMBERS, XXREAL_0, XREAL_0, MEMBERED, SETFAM_1, DOMAIN_1,
XXREAL_2;
registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, MEMBERED;
requirements SUBSET, BOOLE;
begin
definition
mode R_eal is Element of ExtREAL;
end;
definition
redefine func +infty -> R_eal;
redefine func -infty -> R_eal;
end;
::
:: Set of UpperBound and set of LowerBound of X being a subset of ExtREAL
::
definition
let X be ext-real-membered set;
func SetMajorant(X) -> ext-real-membered set means
:: SUPINF_1:def 1
for x being ExtReal holds x in it iff x is UpperBound of X;
end;
registration
let X be ext-real-membered set;
cluster SetMajorant(X) -> non empty;
end;
theorem :: SUPINF_1:1
for X,Y being ext-real-membered set st X c= Y holds for x being
ExtReal holds x in SetMajorant Y implies x in SetMajorant(X);
definition
let X be ext-real-membered set;
func SetMinorant(X) -> ext-real-membered set means
:: SUPINF_1:def 2
for x being ExtReal holds x in it iff x is LowerBound of X;
end;
registration
let X be ext-real-membered set;
cluster SetMinorant(X) -> non empty;
end;
theorem :: SUPINF_1:2
for X,Y being ext-real-membered set st X c= Y holds for x being
ExtReal holds x in SetMinorant(Y) implies x in SetMinorant(X);
::
:: sup X, inf X least upper bound and greatest lower bound of set X
::
theorem :: SUPINF_1:3
for X being non empty ext-real-membered set holds sup X = inf
SetMajorant(X) & inf X = sup SetMinorant(X);
registration
let X be non empty set;
cluster non empty with_non-empty_elements for Subset-Family of X;
end;
definition
let X be non empty set;
mode bool_DOMAIN of X is non empty with_non-empty_elements Subset-Family of
X;
end;
definition
let F be bool_DOMAIN of ExtREAL;
func SUP(F) -> ext-real-membered set means
:: SUPINF_1:def 3
for a being ExtReal
holds a in it iff ex A being non empty ext-real-membered set st A in F &
a = sup A;
end;
registration
let F be bool_DOMAIN of ExtREAL;
cluster SUP(F) -> non empty;
end;
theorem :: SUPINF_1:4
for F being bool_DOMAIN of ExtREAL, S being non empty
ext-real-membered number st S = union F holds sup S is UpperBound of SUP(F);
theorem :: SUPINF_1:5
for F being bool_DOMAIN of ExtREAL, S being ext-real-membered
set st S = union F holds sup SUP(F) is UpperBound of S;
theorem :: SUPINF_1:6
for F being bool_DOMAIN of ExtREAL, S being non empty
ext-real-membered set st S = union F holds sup S = sup SUP(F);
definition
let F be bool_DOMAIN of ExtREAL;
func INF F -> ext-real-membered set means
:: SUPINF_1:def 4
for a being ExtReal
holds a in it iff ex A being non empty ext-real-membered set st A in F &
a = inf A;
end;
registration
let F be bool_DOMAIN of ExtREAL;
cluster INF(F) -> non empty;
end;
theorem :: SUPINF_1:7
for F being bool_DOMAIN of ExtREAL, S being non empty
ext-real-membered set st S = union F holds inf S is LowerBound of INF(F);
theorem :: SUPINF_1:8
for F being bool_DOMAIN of ExtREAL, S being ext-real-membered
set st S = union F holds inf INF(F) is LowerBound of S;
theorem :: SUPINF_1:9
for F being bool_DOMAIN of ExtREAL, S being non empty
ext-real-membered set st S = union F holds inf S = inf INF(F);