:: Some Properties of the Intervals :: by J\'ozef Bia\las :: :: Received February 5, 1994 :: Copyright (c) 1994-2016 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, FUNCT_1, ZFMISC_1, RELAT_1, SUPINF_2, XXREAL_0, CARD_1, SUPINF_1, SUBSET_1, NAT_1, ARYTM_3, ORDINAL1, XXREAL_2, ORDINAL2, XBOOLE_0, REAL_1, ARYTM_1, MEASURE5, XXREAL_1, MEMBERED, MEMBER_1, TARSKI, XCMPLX_0, FREEALG, QUANTAL1, SETFAM_1, FINSET_1, COMPLEX1, SEQ_1, SEQ_2, VALUED_0, SEQ_4, PSCOMP_1, RCOMP_1, PRALG_1, PRE_TOPC, PARTFUN1, INT_1, ASYMPT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, FINSET_1, NUMBERS, MEMBERED, ABSVALUE, COMPLEX1, VALUED_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, MEMBER_1, FUNCT_3, XXREAL_0, XXREAL_1, XXREAL_2, XXREAL_3, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, RCOMP_1, SUPINF_1, SUPINF_2, MEASURE5, VALUED_1; constructors WELLORD2, DOMAIN_1, REAL_1, NAT_1, CARD_1, SUPINF_2, MEASURE5, SUPINF_1, RCOMP_1, RELSET_1, COMPLEX1, SEQ_2, SEQM_3, VALUED_0, VALUED_1, FUNCOP_1, SEQ_4, BINOP_2, LIMFUNC1, MEMBER_1, FUNCT_3, COMSEQ_2, SEQ_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XREAL_0, MEMBERED, XXREAL_1, XXREAL_2, XXREAL_3, VALUED_0, VALUED_1, NAT_1, INT_1, FINSET_1, MEMBER_1, RCOMP_1, SEQ_2, SEQ_4, FCONT_3, FUNCT_2, MEASURE5, RELSET_1, XCMPLX_0, SEQ_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin :: Some theorems about R_eal numbers theorem :: MEASURE6:1 ex F being sequence of [:NAT,NAT:] st F is one-to-one & dom F = NAT & rng F = [:NAT,NAT:]; theorem :: MEASURE6:2 for F being sequence of ExtREAL st F is nonnegative holds 0. <= SUM(F); theorem :: MEASURE6:3 for F being sequence of ExtREAL, x being R_eal st (ex n being Element of NAT st x <= F.n) & F is nonnegative holds x <= SUM(F); definition ::\$CD end; theorem :: MEASURE6:4 for eps being ExtReal st 0. < eps ex F being sequence of ExtREAL st (for n being Nat holds 0. < F.n) & SUM(F) < eps; theorem :: MEASURE6:5 for eps being ExtReal, X being non empty Subset of ExtREAL st 0. < eps & inf X is Real holds ex x being ExtReal st x in X & x < inf X + eps; theorem :: MEASURE6:6 for eps being ExtReal, X being non empty Subset of ExtREAL st 0. < eps & sup X is Real holds ex x being ExtReal st x in X & sup X - eps < x; theorem :: MEASURE6:7 for F being sequence of ExtREAL st F is nonnegative & SUM(F) < +infty holds for n being Element of NAT holds F.n in REAL; :: PROPERTIES OF THE INTERVALS registration cluster non empty interval for Subset of REAL; end; theorem :: MEASURE6:8 for A being non empty Interval, a being ExtReal st ex b being ExtReal st a <= b & A = ].a,b.[ holds a = inf A; theorem :: MEASURE6:9 for A being non empty Interval, a being ExtReal st ex b being ExtReal st a <= b & A = ].a,b.] holds a = inf A; theorem :: MEASURE6:10 for A being non empty Interval, a being ExtReal st ex b being ExtReal st a <= b & A = [.a,b.] holds a = inf A; theorem :: MEASURE6:11 for A being non empty Interval, a being ExtReal st ex b being ExtReal st a <= b & A = [.a,b.[ holds a = inf A; theorem :: MEASURE6:12 for A being non empty Interval, b being ExtReal st ex a being ExtReal st a <= b & A = ].a,b.[ holds b = sup A; theorem :: MEASURE6:13 for A being non empty Interval, b being ExtReal st ex a being ExtReal st a <= b & A = ].a,b.] holds b = sup A; theorem :: MEASURE6:14 for A being non empty Interval, b being ExtReal st ex a being ExtReal st a <= b & A = [.a,b.] holds b = sup A; theorem :: MEASURE6:15 for A being non empty Interval, b being ExtReal st ex a being ExtReal st a <= b & A = [.a,b.[ holds b = sup A; theorem :: MEASURE6:16 for A being non empty Interval st A is open_interval holds A = ].inf A,sup A.[; theorem :: MEASURE6:17 for A being non empty Interval st A is closed_interval holds A = [.inf A,sup A.]; theorem :: MEASURE6:18 for A being non empty Interval st A is right_open_interval holds A = [.inf A,sup A.[; theorem :: MEASURE6:19 for A being non empty Interval st A is left_open_interval holds A = ].inf A,sup A.]; theorem :: MEASURE6:20 for A,B being non empty Interval, a,b being Real st a in A & b in B & sup A <= inf B holds a <= b; theorem :: MEASURE6:21 for A,B be real-membered set holds for y being Real holds y in B ++ A iff ex x,z being Real st x in B & z in A & y = x + z; theorem :: MEASURE6:22 for A,B being non empty Interval holds sup A = inf B & (sup A in A or inf B in B) implies A \/ B is Interval; definition let A be real-membered set; let x be Real; redefine func x ++ A -> Subset of REAL; end; theorem :: MEASURE6:23 for A being Subset of REAL, x being Real holds -x ++ (x ++ A) = A; theorem :: MEASURE6:24 for x being Real, A being Subset of REAL st A = REAL holds x ++ A = A; theorem :: MEASURE6:25 for x being Real holds x ++ {} = {}; theorem :: MEASURE6:26 for A being Interval, x being Real holds A is open_interval iff x ++ A is open_interval; theorem :: MEASURE6:27 for A being Interval, x being Real holds A is closed_interval iff x ++ A is closed_interval; theorem :: MEASURE6:28 for A being Interval, x being Real holds A is right_open_interval iff x ++ A is right_open_interval; theorem :: MEASURE6:29 for A being Interval, x being Real holds A is left_open_interval iff x ++ A is left_open_interval; theorem :: MEASURE6:30 for A being Interval, x being Real holds x ++ A is Interval; theorem :: MEASURE6:31 for A being real-membered set, x being Real, y being R_eal st x = y holds sup(x ++ A) = y + sup A; theorem :: MEASURE6:32 for A being real-membered set, x being Real, y being R_eal st x = y holds inf(x ++ A) = y + inf A; theorem :: MEASURE6:33 for A being Interval, x being Real holds diameter(A) = diameter(x ++ A); begin :: from PSCOMP_1, 2010.02.26, A.T. notation let X be set; synonym X is without_zero for X is with_non-empty_elements; antonym X is with_zero for X is with_non-empty_elements; end; definition let X be set; redefine attr X is without_zero means :: MEASURE6:def 2 not 0 in X; end; registration cluster REAL -> with_zero; cluster NAT -> with_zero; end; registration cluster non empty without_zero for set; cluster non empty with_zero for set; end; registration cluster non empty without_zero for Subset of REAL; cluster non empty with_zero for Subset of REAL; end; theorem :: MEASURE6:34 for F being set st F is non empty with_non-empty_elements c=-linear holds F is centered; registration let F be set; cluster non empty with_non-empty_elements c=-linear -> centered for Subset-Family of F; end; registration ::: FUNCT_2 let X, Y be non empty set, f be Function of X, Y; cluster f.:X -> non empty; end; definition ::: FUNCT_3 let X, Y be set, f be Function of X, Y; func "f -> Function of bool Y, bool X means :: MEASURE6:def 3 for y being Subset of Y holds it.y = f"y; end; theorem :: MEASURE6:35 for X, Y, x being set, S being Subset-Family of Y, f being Function of X, Y st x in meet (("f).:S) holds f.x in meet S; reserve r, s, t for Real; theorem :: MEASURE6:36 ::: SQUARE_1 or ABSVALUE |.r.| + |.s.| = 0 implies r = 0; theorem :: MEASURE6:37 ::: SQUARE_1 or ABSVALUE r < s & s < t implies |.s.| < |.r.| + |.t.|; reserve seq for Real_Sequence, X, Y for Subset of REAL; theorem :: MEASURE6:38 ::: SEQ_2 seq is convergent & seq is non-zero & lim seq = 0 implies seq" is non bounded ; theorem :: MEASURE6:39 ::: SEQ_2 rng seq is real-bounded iff seq is bounded; notation let X be real-membered set; synonym X is with_max for X is right_end; synonym X is with_min for X is left_end; end; definition let X be real-membered set; redefine attr X is with_max means :: MEASURE6:def 4 X is bounded_above & upper_bound X in X; redefine attr X is with_min means :: MEASURE6:def 5 X is bounded_below & lower_bound X in X; end; registration cluster non empty closed real-bounded for Subset of REAL; end; definition let R be Subset-Family of REAL; attr R is open means :: MEASURE6:def 6 for X being Subset of REAL st X in R holds X is open; attr R is closed means :: MEASURE6:def 7 for X being Subset of REAL st X in R holds X is closed; end; reserve r3, r1, q3, p3 for Real; definition let X be Subset of REAL; redefine func --X -> Subset of REAL; end; theorem :: MEASURE6:40 r in X iff -r in --X; theorem :: MEASURE6:41 X is bounded_above iff --X is bounded_below; theorem :: MEASURE6:42 X is bounded_below iff --X is bounded_above; theorem :: MEASURE6:43 for X being non empty Subset of REAL st X is bounded_below holds lower_bound X = - upper_bound --X; theorem :: MEASURE6:44 for X being non empty Subset of REAL st X is bounded_above holds upper_bound X = - lower_bound --X; theorem :: MEASURE6:45 X is closed iff --X is closed; theorem :: MEASURE6:46 r in X iff q3+r in q3++X; theorem :: MEASURE6:47 X = 0++X; theorem :: MEASURE6:48 q3++(p3++X) = (q3+p3)++X; theorem :: MEASURE6:49 X is bounded_above iff q3++X is bounded_above; theorem :: MEASURE6:50 X is bounded_below iff q3++X is bounded_below; theorem :: MEASURE6:51 for X being non empty Subset of REAL st X is bounded_below holds lower_bound (q3++X) = q3+lower_bound X; theorem :: MEASURE6:52 for X being non empty Subset of REAL st X is bounded_above holds upper_bound (q3++X) = q3+upper_bound X; theorem :: MEASURE6:53 X is closed iff q3++X is closed; definition let X be Subset of REAL; func Inv X -> Subset of REAL equals :: MEASURE6:def 8 { 1/r3 : r3 in X }; involutiveness; end; theorem :: MEASURE6:54 for X being Subset of REAL holds r in X iff 1/r in Inv X; registration let X be non empty Subset of REAL; cluster Inv X -> non empty; end; registration let X be without_zero Subset of REAL; cluster Inv X -> without_zero; end; theorem :: MEASURE6:55 for X being without_zero Subset of REAL st X is closed real-bounded holds Inv X is closed; theorem :: MEASURE6:56 for Z being Subset-Family of REAL st Z is closed holds meet Z is closed; definition let X be real-membered set; func Cl X -> Subset of REAL equals :: MEASURE6:def 9 meet { A where A is Subset of REAL : X c= A & A is closed }; projectivity; end; registration let X be real-membered set; cluster Cl X -> closed; end; theorem :: MEASURE6:57 for Y being closed Subset of REAL st X c= Y holds Cl X c= Y; theorem :: MEASURE6:58 for X being real-membered set holds X c= Cl X; theorem :: MEASURE6:59 X is closed iff X = Cl X; theorem :: MEASURE6:60 Cl ({}REAL) = {}; theorem :: MEASURE6:61 Cl ([#]REAL) = REAL; theorem :: MEASURE6:62 for X, Y being real-membered set holds X c= Y implies Cl X c= Cl Y; theorem :: MEASURE6:63 r3 in Cl X iff for O being open Subset of REAL st r3 in O holds O /\ X is non empty; theorem :: MEASURE6:64 r3 in Cl X implies ex seq st rng seq c= X & seq is convergent & lim seq = r3; begin :: Functions into Reals definition let X be set, f be Function of X, REAL; redefine attr f is bounded_below means :: MEASURE6:def 10 f.:X is bounded_below; redefine attr f is bounded_above means :: MEASURE6:def 11 f.:X is bounded_above; end; definition let X be set, f be Function of X, REAL; attr f is with_max means :: MEASURE6:def 12 f.:X is with_max; attr f is with_min means :: MEASURE6:def 13 f.:X is with_min; end; theorem :: MEASURE6:65 for X, A being set, f being Function of X, REAL holds (-f).:A = --(f.:A); theorem :: MEASURE6:66 for X being non empty set, f being Function of X, REAL holds f is with_min iff -f is with_max; theorem :: MEASURE6:67 for X being non empty set, f being Function of X, REAL holds f is with_max iff -f is with_min; theorem :: MEASURE6:68 for X being set, A being Subset of REAL, f being Function of X, REAL holds (-f)"A = f"(--A); theorem :: MEASURE6:69 for X, A being set, f being Function of X, REAL, s being Real holds (s+f).:A = s++(f.:A); theorem :: MEASURE6:70 for X being set, A being Subset of REAL, f being Function of X,REAL, q3 holds (q3+f)"A = f"(-q3++A); notation let f be real-valued Function; synonym Inv f for f"; end; definition let C be set; let D be real-membered set; let f be PartFunc of C,D; redefine func Inv f -> PartFunc of C,REAL; end; theorem :: MEASURE6:71 for X being set, A being without_zero Subset of REAL, f being Function of X, REAL holds (Inv f)"A = f"(Inv A); theorem :: MEASURE6:72 for A being Subset of REAL, x being Real st x in --A holds ex a being Real st a in A & x = -a;