Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

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

Back to top