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