:: Suprema and Infima of Intervals of Extended Real Numbers :: by Andrzej Trybulec :: :: Received June 26, 2008 :: Copyright (c) 2008-2018 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 NUMBERS, INT_1, SUBSET_1, XXREAL_0, FINSET_1, ARYTM_3, XBOOLE_0, ARYTM_1, NAT_1, FUNCT_1, RELAT_1, TARSKI, ORDINAL1, MEMBERED, ORDINAL2, FINSUB_1, SETWISEO, CARD_1, XREAL_0, RAT_1, XXREAL_1, XXREAL_2, MEASURE5, REAL_1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, CARD_1, FINSUB_1, SETWISEO, NUMBERS, MEMBERED, XXREAL_0, XCMPLX_0, XREAL_0, INT_1, NAT_1, RAT_1, XXREAL_1; constructors XXREAL_0, MEMBERED, XREAL_0, INT_1, FINSET_1, RAT_1, XXREAL_1, SETWISEO, XCMPLX_0, REAL_1, NAT_1, XTUPLE_0, CARD_1; registrations XXREAL_0, MEMBERED, XXREAL_1, XBOOLE_0, FINSET_1, NUMBERS, SETWISEO, FINSUB_1, XREAL_0, INT_1, NAT_1, CARD_1, ORDINAL1; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin scheme :: XXREAL_2:sch 1 FinInter{m, n() -> Integer, F(object)->object, P[object]}: {F(i) where i is Element of INT: m()<=i & i<=n() & P[i]} is finite; reserve x,y,z,r,s for ExtReal; definition let X be ext-real-membered set; mode UpperBound of X -> ExtReal means :: XXREAL_2:def 1 x in X implies x <= it; mode LowerBound of X -> ExtReal means :: XXREAL_2:def 2 x in X implies it <= x; end; definition let X be ext-real-membered set; func sup X -> ExtReal means :: XXREAL_2:def 3 it is UpperBound of X & for x being UpperBound of X holds it <= x; func inf X -> ExtReal means :: XXREAL_2:def 4 it is LowerBound of X & for x being LowerBound of X holds x <= it; end; definition let X be ext-real-membered set; attr X is left_end means :: XXREAL_2:def 5 inf X in X; attr X is right_end means :: XXREAL_2:def 6 sup X in X; end; theorem :: XXREAL_2:1 y is UpperBound of {x} iff x <= y; theorem :: XXREAL_2:2 y is LowerBound of {x} iff y <= x; registration cluster -> ext-real-membered for Element of Fin ExtREAL; end; reserve A,B for ext-real-membered set; theorem :: XXREAL_2:3 x in A implies inf A <= x; theorem :: XXREAL_2:4 x in A implies x <= sup A; theorem :: XXREAL_2:5 B c= A implies for x being LowerBound of A holds x is LowerBound of B; theorem :: XXREAL_2:6 B c= A implies for x being UpperBound of A holds x is UpperBound of B; theorem :: XXREAL_2:7 for x being LowerBound of A, y being LowerBound of B holds min(x, y) is LowerBound of A\/ B; theorem :: XXREAL_2:8 for x being UpperBound of A, y being UpperBound of B holds max(x, y) is UpperBound of A\/ B; theorem :: XXREAL_2:9 inf(A \/ B) = min(inf A,inf B); theorem :: XXREAL_2:10 sup(A \/ B) = max(sup A,sup B); registration cluster finite -> left_end right_end for non empty ext-real-membered set; end; registration cluster -> left_end for non empty natural-membered set; end; registration cluster right_end for non empty natural-membered set; end; notation let X be left_end ext-real-membered set; synonym min X for inf X; end; notation let X be right_end ext-real-membered set; synonym max X for sup X; end; definition let X be left_end ext-real-membered set; redefine func min X means :: XXREAL_2:def 7 it in X & for x st x in X holds it <= x; end; definition let X be right_end ext-real-membered set; redefine func max X means :: XXREAL_2:def 8 it in X & for x st x in X holds x <= it; end; theorem :: XXREAL_2:11 max{x} = x; theorem :: XXREAL_2:12 max(x,y) = max{x,y}; theorem :: XXREAL_2:13 min{x} = x; theorem :: XXREAL_2:14 min{x,y} = min(x,y); definition let X be ext-real-membered set; attr X is bounded_below means :: XXREAL_2:def 9 ex r being Real st r is LowerBound of X; attr X is bounded_above means :: XXREAL_2:def 10 ex r being Real st r is UpperBound of X; end; registration cluster non empty finite natural-membered for set; end; definition let X be ext-real-membered set; attr X is real-bounded means :: XXREAL_2:def 11 X is bounded_below bounded_above; end; registration cluster real-bounded -> bounded_above bounded_below for ext-real-membered set; cluster bounded_above bounded_below -> real-bounded for ext-real-membered set; end; registration cluster finite -> real-bounded for real-membered set; end; registration cluster real-bounded for non empty natural-membered set; end; theorem :: XXREAL_2:15 for X being non empty real-membered set st X is bounded_below holds inf X in REAL; theorem :: XXREAL_2:16 for X being non empty real-membered set st X is bounded_above holds sup X in REAL; registration let X be bounded_above non empty real-membered set; cluster sup X -> real; end; registration let X be bounded_below non empty real-membered set; cluster inf X -> real; end; registration cluster bounded_above -> right_end for non empty integer-membered set; end; registration cluster bounded_below -> left_end for non empty integer-membered set; end; registration cluster -> bounded_below for natural-membered set; end; registration let X be left_end real-membered set; cluster min X -> real; end; registration let X be left_end rational-membered set; cluster min X -> rational; end; registration let X be left_end integer-membered set; cluster min X -> integer; end; registration let X be left_end natural-membered set; cluster min X -> natural; end; registration let X be right_end real-membered set; cluster max X -> real; end; registration let X be right_end rational-membered set; cluster max X -> rational; end; registration let X be right_end integer-membered set; cluster max X -> integer; end; registration let X be right_end natural-membered set; cluster max X -> natural; end; registration cluster left_end -> bounded_below for real-membered set; cluster right_end -> bounded_above for real-membered set; end; theorem :: XXREAL_2:17 x is LowerBound of [.x,y.]; theorem :: XXREAL_2:18 x is LowerBound of ].x,y.]; theorem :: XXREAL_2:19 x is LowerBound of [.x,y.[; theorem :: XXREAL_2:20 x is LowerBound of ].x,y.[; theorem :: XXREAL_2:21 y is UpperBound of [.x,y.]; theorem :: XXREAL_2:22 y is UpperBound of ].x,y.]; theorem :: XXREAL_2:23 y is UpperBound of [.x,y.[; theorem :: XXREAL_2:24 y is UpperBound of ].x,y.[; theorem :: XXREAL_2:25 x <= y implies inf [.x,y.] = x; theorem :: XXREAL_2:26 x < y implies inf [.x,y.[ = x; theorem :: XXREAL_2:27 x < y implies inf ].x,y.] = x; theorem :: XXREAL_2:28 x < y implies inf ].x,y.[ = x; theorem :: XXREAL_2:29 x <= y implies sup [.x,y.] = y; theorem :: XXREAL_2:30 x < y implies sup ].x,y.] = y; theorem :: XXREAL_2:31 x < y implies sup [.x,y.[ = y; theorem :: XXREAL_2:32 x < y implies sup ].x,y.[ = y; theorem :: XXREAL_2:33 x <= y implies [.x,y.] is left_end right_end; theorem :: XXREAL_2:34 x < y implies [.x,y.[ is left_end; theorem :: XXREAL_2:35 x < y implies ].x,y.] is right_end; theorem :: XXREAL_2:36 x is LowerBound of {}; theorem :: XXREAL_2:37 x is UpperBound of {}; theorem :: XXREAL_2:38 inf {} = +infty; theorem :: XXREAL_2:39 sup {} = -infty; theorem :: XXREAL_2:40 for X being ext-real-membered set holds X is non empty iff inf X <= sup X; registration cluster real-bounded -> finite for integer-membered set; end; registration cluster -> finite for bounded_above natural-membered set; end; theorem :: XXREAL_2:41 for X being ext-real-membered set holds +infty is UpperBound of X; theorem :: XXREAL_2:42 for X being ext-real-membered set holds -infty is LowerBound of X; theorem :: XXREAL_2:43 for X,Y being ext-real-membered set st X c= Y & Y is bounded_above holds X is bounded_above; theorem :: XXREAL_2:44 for X,Y being ext-real-membered set st X c= Y & Y is bounded_below holds X is bounded_below; theorem :: XXREAL_2:45 for X,Y being ext-real-membered set st X c= Y & Y is real-bounded holds X is real-bounded; theorem :: XXREAL_2:46 REAL is non bounded_below non bounded_above; registration cluster REAL -> non bounded_below non bounded_above; end; theorem :: XXREAL_2:47 {+infty} is bounded_below; theorem :: XXREAL_2:48 {-infty} is bounded_above; theorem :: XXREAL_2:49 for X being bounded_above non empty ext-real-membered set st X <> {-infty} holds ex x being Element of REAL st x in X; theorem :: XXREAL_2:50 for X being bounded_below non empty ext-real-membered set st X <> {+infty} holds ex x being Element of REAL st x in X; theorem :: XXREAL_2:51 for X being ext-real-membered set st -infty is UpperBound of X holds X c= {-infty}; theorem :: XXREAL_2:52 for X being ext-real-membered set st +infty is LowerBound of X holds X c= {+infty}; theorem :: XXREAL_2:53 for X being non empty ext-real-membered set st ex y being UpperBound of X st y <> +infty holds X is bounded_above; theorem :: XXREAL_2:54 for X being non empty ext-real-membered set st ex y being LowerBound of X st y <> -infty holds X is bounded_below; theorem :: XXREAL_2:55 for X being non empty ext-real-membered set, x being UpperBound of X st x in X holds x = sup X; theorem :: XXREAL_2:56 for X being non empty ext-real-membered set, x being LowerBound of X st x in X holds x = inf X; theorem :: XXREAL_2:57 for X being non empty ext-real-membered set st X is bounded_above & X <> {-infty} holds sup X in REAL; theorem :: XXREAL_2:58 for X being non empty ext-real-membered set st X is bounded_below & X <> {+infty} holds inf X in REAL; theorem :: XXREAL_2:59 for X,Y being ext-real-membered set st X c= Y holds sup X <= sup Y; theorem :: XXREAL_2:60 for X,Y being ext-real-membered set st X c= Y holds inf Y <= inf X; theorem :: XXREAL_2:61 for X being ext-real-membered set, x being ExtReal st (ex y being ExtReal st y in X & x <= y) holds x <= sup X; theorem :: XXREAL_2:62 for X being ext-real-membered set, x being ExtReal st (ex y being ExtReal st y in X & y <= x) holds inf X <= x; theorem :: XXREAL_2:63 for X,Y being ext-real-membered set st for x being ExtReal st x in X ex y being ExtReal st y in Y & x <= y holds sup X <= sup Y; theorem :: XXREAL_2:64 for X,Y being ext-real-membered set st for y being ExtReal st y in Y ex x being ExtReal st x in X & x <= y holds inf X <= inf Y; theorem :: XXREAL_2:65 for X,Y being ext-real-membered set, x being UpperBound of X, y being UpperBound of Y holds min(x,y) is UpperBound of X /\ Y; theorem :: XXREAL_2:66 for X,Y being ext-real-membered set, x being LowerBound of X, y being LowerBound of Y holds max(x,y) is LowerBound of X /\ Y; theorem :: XXREAL_2:67 for X,Y being ext-real-membered set holds sup(X /\ Y) <= min(sup X,sup Y); theorem :: XXREAL_2:68 for X,Y being ext-real-membered set holds max(inf X,inf Y) <= inf(X /\ Y); registration cluster real-bounded -> real-membered for ext-real-membered set; end; theorem :: XXREAL_2:69 A c= [.inf A, sup A.]; theorem :: XXREAL_2:70 sup A = inf A implies A = {inf A}; theorem :: XXREAL_2:71 x <= y & x is UpperBound of A implies y is UpperBound of A; theorem :: XXREAL_2:72 y <= x & x is LowerBound of A implies y is LowerBound of A; theorem :: XXREAL_2:73 A is bounded_above iff sup A <> +infty; theorem :: XXREAL_2:74 A is bounded_below iff inf A <> -infty; begin :: Connectedness definition let A be ext-real-membered set; attr A is interval means :: XXREAL_2:def 12 for r,s being ExtReal st r in A & s in A holds [.r,s.] c= A; end; registration cluster ExtREAL -> interval; cluster empty -> interval for ext-real-membered set; let r,s; cluster [.r,s.] -> interval; cluster ].r,s.] -> interval; cluster [.r,s.[ -> interval; cluster ].r,s.[ -> interval; end; registration cluster REAL -> interval; end; registration cluster interval for non empty ext-real-membered set; end; registration let A,B be interval ext-real-membered set; cluster A /\ B -> interval; end; reserve A,B for ext-real-membered set; registration let r,s; cluster ].r,s.] -> non left_end; cluster [.r,s.[ -> non right_end; cluster ].r,s.[ -> non left_end non right_end; end; registration cluster left_end right_end interval for ext-real-membered set; cluster non left_end right_end interval for ext-real-membered set; cluster left_end non right_end interval for ext-real-membered set; cluster non left_end non right_end interval non empty for ext-real-membered set; end; theorem :: XXREAL_2:75 for A being left_end right_end interval ext-real-membered set holds A = [.min A, max A.]; theorem :: XXREAL_2:76 for A being non left_end right_end interval ext-real-membered set holds A = ].inf A, max A.]; theorem :: XXREAL_2:77 for A being left_end non right_end interval ext-real-membered set holds A = [.min A, sup A.[; theorem :: XXREAL_2:78 for A being non left_end non right_end non empty interval ext-real-membered set holds A =].inf A,sup A.[; theorem :: XXREAL_2:79 for A being non left_end non right_end interval ext-real-membered set ex r,s st r <= s & A =].r,s.[; theorem :: XXREAL_2:80 A is interval implies for x,y,r st x in A & y in A & x <= r & r <= y holds r in A; theorem :: XXREAL_2:81 A is interval implies for x,r st x in A & x <= r & r < sup A holds r in A; theorem :: XXREAL_2:82 A is interval implies for x,r st x in A & inf A < r & r <= x holds r in A; theorem :: XXREAL_2:83 A is interval implies for r st inf A < r & r < sup A holds r in A; theorem :: XXREAL_2:84 (for x,y,r st x in A & y in A & x < r & r < y holds r in A) implies A is interval; theorem :: XXREAL_2:85 (for x,r st x in A & x < r & r < sup A holds r in A) implies A is interval; theorem :: XXREAL_2:86 (for y,r st y in A & inf A < r & r < y holds r in A) implies A is interval; theorem :: XXREAL_2:87 (for r st inf A < r & r < sup A holds r in A) implies A is interval; theorem :: XXREAL_2:88 (for x,y,r st x in A & y in A & x <= r & r <= y holds r in A) implies A is interval; theorem :: XXREAL_2:89 A is interval & B is interval & A meets B implies A \/ B is interval; theorem :: XXREAL_2:90 A is interval & B is left_end interval & sup A = inf B implies A \/ B is interval; theorem :: XXREAL_2:91 A is right_end interval & B is interval & sup A = inf B implies A \/ B is interval; registration cluster left_end -> non empty for ext-real-membered set; cluster right_end -> non empty for ext-real-membered set; end; :: from HAHNBAN, 2011.04.26, A.T. theorem :: XXREAL_2:92 for A being non empty Subset of ExtREAL st for r being Element of ExtREAL st r in A holds r <= -infty holds A = {-infty}; theorem :: XXREAL_2:93 for A being non empty Subset of ExtREAL st for r being Element of ExtREAL st r in A holds +infty <= r holds A = {+infty}; theorem :: XXREAL_2:94 for A being non empty Subset of ExtREAL, r being ExtReal st r < sup A ex s being Element of ExtREAL st s in A & r < s; theorem :: XXREAL_2:95 for A being non empty Subset of ExtREAL, r being Element of ExtREAL st inf A < r ex s being Element of ExtREAL st s in A & s < r; theorem :: XXREAL_2:96 for A,B being non empty Subset of ExtREAL st for r,s being ExtReal st r in A & s in B holds r <= s holds sup A <= inf B;