:: Properties of the Intervals of Real Numbers :: by J\'ozef Bia{\l}as :: :: Received January 12, 1993 :: Copyright (c) 1993-2012 Association of Mizar Users begin scheme :: MEASURE5:sch 1 RSetEq{ P1[ set ] } : for X1, X2 being Subset of REAL st ( for x being R_eal holds ( x in X1 iff P1[x] ) ) & ( for x being R_eal holds ( x in X2 iff P1[x] ) ) holds X1 = X2 proofend; definition let a, b be R_eal; :: original:]. redefine func].a,b.[ -> Subset of REAL means :: MEASURE5:def 1 for x being R_eal holds ( x in it iff ( a < x & x < b ) ); coherence ].a,b.[ is Subset of REAL proofend; compatibility for b1 being Subset of REAL holds ( b1 = ].a,b.[ iff for x being R_eal holds ( x in b1 iff ( a < x & x < b ) ) ) proofend; end; :: deftheorem defines ]. MEASURE5:def_1_:_ for a, b being R_eal for b3 being Subset of REAL holds ( b3 = ].a,b.[ iff for x being R_eal holds ( x in b3 iff ( a < x & x < b ) ) ); definition let IT be Subset of REAL; attrIT is open_interval means :Def2: :: MEASURE5:def 2 ex a, b being R_eal st IT = ].a,b.[; attrIT is closed_interval means :Def3: :: MEASURE5:def 3 ex a, b being real number st IT = [.a,b.]; end; :: deftheorem Def2 defines open_interval MEASURE5:def_2_:_ for IT being Subset of REAL holds ( IT is open_interval iff ex a, b being R_eal st IT = ].a,b.[ ); :: deftheorem Def3 defines closed_interval MEASURE5:def_3_:_ for IT being Subset of REAL holds ( IT is closed_interval iff ex a, b being real number st IT = [.a,b.] ); registration cluster non empty complex-membered ext-real-membered real-membered open_interval for Element of K32(REAL); existence ex b1 being Subset of REAL st ( not b1 is empty & b1 is open_interval ) proofend; cluster non empty complex-membered ext-real-membered real-membered closed_interval for Element of K32(REAL); existence ex b1 being Subset of REAL st ( not b1 is empty & b1 is closed_interval ) proofend; end; definition let IT be Subset of REAL; attrIT is right_open_interval means :Def4: :: MEASURE5:def 4 ex a being real number ex b being R_eal st IT = [.a,b.[; end; :: deftheorem Def4 defines right_open_interval MEASURE5:def_4_:_ for IT being Subset of REAL holds ( IT is right_open_interval iff ex a being real number ex b being R_eal st IT = [.a,b.[ ); notation let IT be Subset of REAL; synonym left_closed_interval IT for right_open_interval ; end; definition let IT be Subset of REAL; attrIT is left_open_interval means :Def5: :: MEASURE5:def 5 ex a being R_eal ex b being real number st IT = ].a,b.]; end; :: deftheorem Def5 defines left_open_interval MEASURE5:def_5_:_ for IT being Subset of REAL holds ( IT is left_open_interval iff ex a being R_eal ex b being real number st IT = ].a,b.] ); notation let IT be Subset of REAL; synonym right_closed_interval IT for left_open_interval ; end; registration cluster non empty complex-membered ext-real-membered real-membered right_open_interval for Element of K32(REAL); existence ex b1 being Subset of REAL st ( not b1 is empty & b1 is right_open_interval ) proofend; cluster non empty complex-membered ext-real-membered real-membered left_open_interval for Element of K32(REAL); existence ex b1 being Subset of REAL st ( not b1 is empty & b1 is left_open_interval ) proofend; end; definition mode Interval is interval Subset of REAL; end; registration cluster open_interval -> interval for Element of K32(REAL); coherence for b1 being Subset of REAL st b1 is open_interval holds b1 is interval proofend; cluster closed_interval -> interval for Element of K32(REAL); coherence for b1 being Subset of REAL st b1 is closed_interval holds b1 is interval proofend; cluster right_open_interval -> interval for Element of K32(REAL); coherence for b1 being Subset of REAL st b1 is right_open_interval holds b1 is interval proofend; cluster left_open_interval -> interval for Element of K32(REAL); coherence for b1 being Subset of REAL st b1 is left_open_interval holds b1 is interval proofend; end; theorem :: MEASURE5:1 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 ) proofend; theorem Th2: :: MEASURE5:2 for a, b being R_eal st a < b holds ex x being R_eal st ( a < x & x < b & x in REAL ) proofend; theorem :: MEASURE5:3 for a, b, c being R_eal st a < b & a < c holds ex x being R_eal st ( a < x & x < b & x < c & x in REAL ) proofend; theorem :: MEASURE5:4 for a, b, c being R_eal st a < c & b < c holds ex x being R_eal st ( a < x & b < x & x < c & x in REAL ) proofend; definition let A be ext-real-membered set ; func diameter A -> R_eal equals :Def6: :: MEASURE5:def 6 (sup A) - (inf A) if A <> {} otherwise 0. ; coherence ( ( A <> {} implies (sup A) - (inf A) is R_eal ) & ( not A <> {} implies 0. is R_eal ) ) ; consistency for b1 being R_eal holds verum ; end; :: deftheorem Def6 defines diameter MEASURE5:def_6_:_ for A being ext-real-membered set holds ( ( A <> {} implies diameter A = (sup A) - (inf A) ) & ( not A <> {} implies diameter A = 0. ) ); theorem :: MEASURE5:5 for a, b being R_eal holds ( ( a < b implies diameter ].a,b.[ = b - a ) & ( b <= a implies diameter ].a,b.[ = 0. ) ) proofend; theorem :: MEASURE5:6 for a, b being R_eal holds ( ( a <= b implies diameter [.a,b.] = b - a ) & ( b < a implies diameter [.a,b.] = 0. ) ) proofend; theorem :: MEASURE5:7 for a, b being R_eal holds ( ( a < b implies diameter [.a,b.[ = b - a ) & ( b <= a implies diameter [.a,b.[ = 0. ) ) proofend; theorem :: MEASURE5:8 for a, b being R_eal holds ( ( a < b implies diameter ].a,b.] = b - a ) & ( b <= a implies diameter ].a,b.] = 0. ) ) proofend; theorem :: MEASURE5:9 for A being Interval for a, b being R_eal st a = -infty & b = +infty & ( A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.] ) holds diameter A = +infty proofend; registration cluster empty -> open_interval for Element of K32(REAL); coherence for b1 being Subset of REAL st b1 is empty holds b1 is open_interval proofend; end; theorem :: MEASURE5:10 diameter {} = 0. by Def6; Lm1: for A being Interval holds diameter A >= 0 proofend; Lm2: for A, B being Interval st A c= B holds diameter A <= diameter B proofend; theorem :: MEASURE5:11 for a, b being R_eal for A, B being Interval st A c= B & B = [.a,b.] & b <= a holds ( diameter A = 0. & diameter B = 0. ) proofend; theorem :: MEASURE5:12 for A, B being Interval st A c= B holds diameter A <= diameter B by Lm2; theorem :: MEASURE5:13 for A being Interval holds 0. <= diameter A by Lm1; theorem :: MEASURE5:14 for X being Subset of REAL holds ( ( not X is empty & X is closed_interval ) iff ex a, b being Real st ( a <= b & X = [.a,b.] ) ) proofend;