:: Properties of the Intervals of Real Numbers :: by J\'ozef Bia{\l}as :: :: Received January 12, 1993 :: Copyright (c) 1993-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, SUPINF_1, SUBSET_1, TARSKI, XXREAL_1, ARYTM_3, XXREAL_0, CARD_1, XXREAL_2, ORDINAL2, REAL_1, SUPINF_2, MEMBERED, ARYTM_1, XBOOLE_0, MEASURE5, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0, XREAL_0, REAL_1, XXREAL_1, RCOMP_1, XXREAL_2, SUPINF_1, SUPINF_2; constructors DOMAIN_1, REAL_1, RCOMP_1, SUPINF_2, SUPINF_1, FINSET_1; registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, XXREAL_1, XXREAL_2, SUBSET_1, FINSET_1, ORDINAL1; requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL; definitions MEMBERED, XBOOLE_0; equalities XXREAL_1, XXREAL_3; theorems TARSKI, XREAL_0, XBOOLE_0, XREAL_1, XXREAL_0, NUMBERS, XXREAL_1, XXREAL_2, XXREAL_3; begin :: Some theorems about R_eal numbers reserve a,b for R_eal; :: PROPERTIES OF THE INTERVALS scheme RSetEq {P[set]} : for X1,X2 being Subset of REAL st (for x being R_eal holds x in X1 iff P[x]) & (for x being R_eal holds x in X2 iff P[x]) holds X1 = X2 proof let A1,A2 be Subset of REAL such that A1: for x being R_eal holds x in A1 iff P[x] and A2: for x being R_eal holds x in A2 iff P[x]; thus A1 c= A2 proof let x be Real; assume A3: x in A1; then x in REAL; then reconsider x as R_eal by NUMBERS:31; P[x] by A1,A3; hence thesis by A2; end; let x be Real; assume A4: x in A2; then x in REAL; then reconsider x as R_eal by NUMBERS:31; P[x] by A2,A4; hence thesis by A1; end; definition let a,b be R_eal; redefine func ].a,b.[ -> Subset of REAL means for x being R_eal holds x in it iff a < x & x < b; coherence proof for x being set st x in ]. a,b .[ holds x in REAL; hence thesis; end; compatibility proof let X be Subset of REAL; thus X = ].a,b.[ implies for x being R_eal holds x in X iff a < x & x < b by XXREAL_1:4; assume A1: for x being R_eal holds x in X iff a < x & x < b; thus X c= ].a,b.[ proof let x be Real; assume A2: x in X; then x in REAL; then reconsider t=x as R_eal by NUMBERS:31; a < t & t < b by A1,A2; hence thesis; end; let x be Real; reconsider t=x as R_eal by XXREAL_0:def 1; assume x in ].a,b.[; then a < t & t < b by XXREAL_1:4; hence thesis by A1; end; end; definition let IT be Subset of REAL; attr IT is open_interval means ex a,b being R_eal st IT = ].a,b.[; attr IT is closed_interval means ex a,b being Real st IT = [.a,b.]; end; registration cluster non empty open_interval for Subset of REAL; existence proof take ].-infty,+infty.[; In(0,REAL) in ].-infty,+infty.[ by XXREAL_1:224; hence ].-infty,+infty.[ is non empty; take -infty,+infty; thus thesis; end; cluster non empty closed_interval for Subset of REAL; existence proof take [.0,1.]; thus [.0,1.] is non empty by XXREAL_1:30; take 0,1; thus thesis; end; end; definition let IT be Subset of REAL; attr IT is right_open_interval means ex a being Real, b being R_eal st IT = [.a,b.[; end; notation let IT be Subset of REAL; synonym IT is left_closed_interval for IT is right_open_interval; end; definition let IT be Subset of REAL; attr IT is left_open_interval means ex a being R_eal,b being Real st IT = ].a,b.]; end; notation let IT be Subset of REAL; synonym IT is right_closed_interval for IT is left_open_interval; end; registration cluster non empty right_open_interval for Subset of REAL; existence proof take [.0,+infty.[; 0 in [.0,+infty.[ by XXREAL_1:236; hence [.0,+infty.[ is non empty; take 0,+infty; thus thesis; end; cluster non empty left_open_interval for Subset of REAL; existence proof take ].-infty,1.]; 1 in ].-infty,1.] by XXREAL_1:234; hence ].-infty,1.] is non empty; take -infty,1; thus thesis; end; end; definition mode Interval is interval Subset of REAL; end; reserve A,B for Interval; registration cluster open_interval -> interval for Subset of REAL; coherence; cluster closed_interval -> interval for Subset of REAL; coherence; cluster right_open_interval -> interval for Subset of REAL; coherence; cluster left_open_interval -> interval for Subset of REAL; coherence; end; theorem for I being interval Subset of REAL holds I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval proof let I be interval Subset of REAL; per cases; suppose A1: I is left_end right_end; reconsider a = inf I,b = sup I as R_eal; A2: a in I & I = [.a,b.] by A1,XXREAL_2:75,def 5; thus thesis by A1,A2; end; suppose A3: I is non left_end right_end; set a = inf I, b = sup I; A4: I = ].a,b.] by A3,XXREAL_2:76; A5: b in I by A3,XXREAL_2:def 6; thus thesis by A5,A4; end; suppose A6: I is left_end non right_end; set a = inf I, b = sup I; A7: I = [.a,b.[ by A6,XXREAL_2:77; A8: a in I by A6,XXREAL_2:def 5; thus thesis by A8,A7; end; suppose I is non left_end non right_end; then consider a,b being ExtReal such that A9: a <= b and A10: I = ].a,b.[ by XXREAL_2:79; reconsider a,b as R_eal by XXREAL_0:def 1; a <= b by A9; hence thesis by A10; end; end; theorem Th2: for a,b being R_eal st a < b ex x being R_eal st a < x & x < b & x in REAL proof let a,b be R_eal; A1: a in REAL or a in {-infty,+infty} by XBOOLE_0:def 3,XXREAL_0:def 4; A2: b in REAL or b in {-infty,+infty} by XBOOLE_0:def 3,XXREAL_0:def 4; assume A3: a < b; then A4: ( not a = +infty)& not b = -infty by XXREAL_0:4,6; per cases by A1,A2,A4,TARSKI:def 2; suppose a in REAL & b in REAL; then consider x,y being Real such that A5: x = a & y = b and x<=y by A3; consider z being Real such that A6: x R_eal equals :Def6: sup A - inf A if A <> {} otherwise 0.; coherence; consistency; end; theorem for a,b being R_eal holds (a < b implies diameter ].a,b.[ = b - a) & ( b <= a implies diameter ].a,b.[ = 0.) proof let a,b being R_eal; hereby assume A1: a < b; then A2: sup ].a,b.[ = b by XXREAL_2:32; ].a,b.[ <> {} & inf ].a,b.[ = a by A1,XXREAL_1:33,XXREAL_2:28; hence diameter ].a,b.[ = b - a by A2,Def6; end; assume b <= a; then ].a,b.[ = {} by XXREAL_1:28; hence thesis by Def6; end; theorem for a,b being R_eal holds (a <= b implies diameter [.a,b.] = b - a) & (b < a implies diameter [.a,b.] = 0.) proof let a,b being R_eal; hereby assume A1: a <= b; then A2: sup [.a,b.] = b by XXREAL_2:29; [.a,b.] <> {} & inf [.a,b.] = a by A1,XXREAL_1:30,XXREAL_2:25; hence diameter [.a,b.] = b - a by A2,Def6; end; assume b < a; then [.a,b.] = {} by XXREAL_1:29; hence thesis by Def6; end; theorem for a,b being R_eal holds (a < b implies diameter [.a,b.[ = b - a) & ( b <= a implies diameter [.a,b.[ = 0.) proof let a,b being R_eal; hereby assume A1: a < b; then A2: sup [.a,b.[ = b by XXREAL_2:31; [.a,b.[ <> {} & inf [.a,b.[ = a by A1,XXREAL_1:31,XXREAL_2:26; hence diameter [.a,b.[ = b - a by A2,Def6; end; assume b <= a; then [.a,b.[ = {} by XXREAL_1:27; hence thesis by Def6; end; theorem for a,b being R_eal holds (a < b implies diameter ].a,b.] = b - a) & ( b <= a implies diameter ].a,b.] = 0.) proof let a,b being R_eal; hereby assume A1: a < b; then A2: sup ].a,b.] = b by XXREAL_2:30; ].a,b.] <> {} & inf ].a,b.] = a by A1,XXREAL_1:32,XXREAL_2:27; hence diameter ].a,b.] = b - a by A2,Def6; end; assume b <= a; then ].a,b.] = {} by XXREAL_1:26; hence thesis by Def6; end; theorem for a,b being R_eal holds a = -infty & b = +infty & (A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.]) implies diameter(A) = +infty proof let a,b be R_eal; assume that A1: a = -infty & b = +infty and A2: A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.]; A3: sup A = +infty & inf A = -infty by A1,A2,XXREAL_2:25,26,27,28,29,30,31,32; then A is non empty by XXREAL_2:40; then diameter(A) = b - a by A1,A3,Def6 .= +infty by A1,XXREAL_3:13; hence thesis; end; registration cluster empty -> open_interval for Subset of REAL; coherence proof let S be Subset of REAL; assume S is empty; then S = ].0.,0..[; hence thesis; end; end; theorem diameter {} = 0. by Def6; Lm1: diameter A >= 0 proof per cases; suppose A is empty; hence thesis by Def6; end; suppose A is non empty; then inf A <= sup A by XXREAL_2:40; then sup A - inf A >= 0 by XXREAL_3:40; hence thesis by Def6; end; end; Lm2: A c= B implies diameter A <= diameter B proof assume A1: A c= B; per cases; suppose A = {}; then diameter A = 0 by Def6; hence thesis by Lm1; end; suppose A2: A <> {}; then B <> {} by A1; then A3: diameter B = sup B - inf B by Def6; A4: sup A <= sup B & inf B <= inf A by A1,XXREAL_2:59,60; diameter A = sup A - inf A by A2,Def6; hence thesis by A3,A4,XXREAL_3:37; end; end; theorem A c= B & B =[.a,b.] & b <= a implies diameter(A) = 0. & diameter(B) = 0. proof assume that A1: A c= B and A2: B =[.a,b.] and A3: b <= a; per cases by A3,XXREAL_0:1; suppose A4: a = b; then B = {a} by A2,XXREAL_1:17; then inf B = a & sup B = a by XXREAL_2:11,13; then A5: diameter B = a - a by A2,A4,Def6 .= 0 by XXREAL_3:7; then diameter A <= 0 by A1,Lm2; hence thesis by A5,Lm1; end; suppose b < a; then A6: B = {} by A2,XXREAL_1:29; then A = {} by A1; hence thesis by A6,Def6; end; end; theorem A c= B implies diameter A <= diameter B by Lm2; theorem 0. <= diameter A by Lm1; theorem for X being Subset of REAL holds X is non empty closed_interval iff ex a,b being Real st a <= b & X = [.a,b.] by XXREAL_1:29,XXREAL_1:30;