:: MEASURE5 semantic presentation 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 proof let A1, A2 be Subset of REAL; ::_thesis: ( ( for x being R_eal holds ( x in A1 iff P1[x] ) ) & ( for x being R_eal holds ( x in A2 iff P1[x] ) ) implies A1 = A2 ) assume that A1: for x being R_eal holds ( x in A1 iff P1[x] ) and A2: for x being R_eal holds ( x in A2 iff P1[x] ) ; ::_thesis: A1 = A2 thus A1 c= A2 :: according to XBOOLE_0:def_10 ::_thesis: A2 c= A1 proof let x be real number ; :: according to MEMBERED:def_9 ::_thesis: ( not x in A1 or x in A2 ) assume A3: x in A1 ; ::_thesis: x in A2 then x in REAL ; then reconsider x = x as R_eal by NUMBERS:31; P1[x] by A1, A3; hence x in A2 by A2; ::_thesis: verum end; let x be real number ; :: according to MEMBERED:def_9 ::_thesis: ( not x in A2 or x in A1 ) assume A4: x in A2 ; ::_thesis: x in A1 then x in REAL ; then reconsider x = x as R_eal by NUMBERS:31; P1[x] by A2, A4; hence x in A1 by A1; ::_thesis: verum end; 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 proof for x being set st x in ].a,b.[ holds x in REAL ; hence ].a,b.[ is Subset of REAL ; ::_thesis: verum end; 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 ) ) ) proof let X be Subset of REAL; ::_thesis: ( X = ].a,b.[ iff for x being R_eal holds ( x in X iff ( a < x & x < b ) ) ) thus ( X = ].a,b.[ implies for x being R_eal holds ( x in X iff ( a < x & x < b ) ) ) by XXREAL_1:4; ::_thesis: ( ( for x being R_eal holds ( x in X iff ( a < x & x < b ) ) ) implies X = ].a,b.[ ) assume A1: for x being R_eal holds ( x in X iff ( a < x & x < b ) ) ; ::_thesis: X = ].a,b.[ thus X c= ].a,b.[ :: according to XBOOLE_0:def_10 ::_thesis: ].a,b.[ c= X proof let x be real number ; :: according to MEMBERED:def_9 ::_thesis: ( not x in X or x in ].a,b.[ ) assume A2: x in X ; ::_thesis: x in ].a,b.[ then x in REAL ; then reconsider t = x as R_eal by NUMBERS:31; ( a < t & t < b ) by A1, A2; hence x in ].a,b.[ ; ::_thesis: verum end; let x be real number ; :: according to MEMBERED:def_9 ::_thesis: ( not x in ].a,b.[ or x in X ) reconsider t = x as R_eal by XXREAL_0:def_1; assume x in ].a,b.[ ; ::_thesis: x in X then ( a < t & t < b ) by XXREAL_1:4; hence x in X by A1; ::_thesis: verum end; 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 ) proof take ].-infty,+infty.[ ; ::_thesis: ( not ].-infty,+infty.[ is empty & ].-infty,+infty.[ is open_interval ) 0 in ].-infty,+infty.[ by XXREAL_1:224; hence not ].-infty,+infty.[ is empty ; ::_thesis: ].-infty,+infty.[ is open_interval take -infty ; :: according to MEASURE5:def_2 ::_thesis: ex b being R_eal st ].-infty,+infty.[ = ].-infty,b.[ take +infty ; ::_thesis: ].-infty,+infty.[ = ].-infty,+infty.[ thus ].-infty,+infty.[ = ].-infty,+infty.[ ; ::_thesis: verum end; 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 ) proof take [.0,1.] ; ::_thesis: ( not [.0,1.] is empty & [.0,1.] is closed_interval ) thus not [.0,1.] is empty by XXREAL_1:30; ::_thesis: [.0,1.] is closed_interval take 0 ; :: according to MEASURE5:def_3 ::_thesis: ex b being real number st [.0,1.] = [.0,b.] take 1 ; ::_thesis: [.0,1.] = [.0,1.] thus [.0,1.] = [.0,1.] ; ::_thesis: verum end; 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 ) proof take [.0,+infty.[ ; ::_thesis: ( not [.0,+infty.[ is empty & [.0,+infty.[ is right_open_interval ) 0 in [.0,+infty.[ by XXREAL_1:236; hence not [.0,+infty.[ is empty ; ::_thesis: [.0,+infty.[ is right_open_interval take 0 ; :: according to MEASURE5:def_4 ::_thesis: ex b being R_eal st [.0,+infty.[ = [.0,b.[ take +infty ; ::_thesis: [.0,+infty.[ = [.0,+infty.[ thus [.0,+infty.[ = [.0,+infty.[ ; ::_thesis: verum end; 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 ) proof take ].-infty,1.] ; ::_thesis: ( not ].-infty,1.] is empty & ].-infty,1.] is left_open_interval ) 1 in ].-infty,1.] by XXREAL_1:234; hence not ].-infty,1.] is empty ; ::_thesis: ].-infty,1.] is left_open_interval take -infty ; :: according to MEASURE5:def_5 ::_thesis: ex b being real number st ].-infty,1.] = ].-infty,b.] take 1 ; ::_thesis: ].-infty,1.] = ].-infty,1.] thus ].-infty,1.] = ].-infty,1.] ; ::_thesis: verum end; 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 proof let I be Subset of REAL; ::_thesis: ( I is open_interval implies I is interval ) assume ex a, b being R_eal st I = ].a,b.[ ; :: according to MEASURE5:def_2 ::_thesis: I is interval hence I is interval ; ::_thesis: verum end; 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 proof let I be Subset of REAL; ::_thesis: ( I is closed_interval implies I is interval ) assume ex a, b being real number st I = [.a,b.] ; :: according to MEASURE5:def_3 ::_thesis: I is interval hence I is interval ; ::_thesis: verum end; 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 proof let I be Subset of REAL; ::_thesis: ( I is right_open_interval implies I is interval ) assume ex a being real number ex b being R_eal st I = [.a,b.[ ; :: according to MEASURE5:def_4 ::_thesis: I is interval hence I is interval ; ::_thesis: verum end; 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 proof let I be Subset of REAL; ::_thesis: ( I is left_open_interval implies I is interval ) assume ex a being R_eal ex b being real number st I = ].a,b.] ; :: according to MEASURE5:def_5 ::_thesis: I is interval hence I is interval ; ::_thesis: verum end; 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 ) proof let I be interval Subset of REAL; ::_thesis: ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) percases ( ( I is left_end & I is right_end ) or ( not I is left_end & I is right_end ) or ( I is left_end & not I is right_end ) or ( not I is left_end & not I is right_end ) ) ; supposeA1: ( I is left_end & I is right_end ) ; ::_thesis: ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) reconsider a = inf I, b = sup I as R_eal ; A2: ( a in I & I = [.a,b.] ) by A1, XXREAL_2:75, XXREAL_2:def_5; thus ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by A1, A2, Def3; ::_thesis: verum end; supposeA3: ( not I is left_end & I is right_end ) ; ::_thesis: ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) set a = inf I; set b = sup I; A4: I = ].(inf I),(sup I).] by A3, XXREAL_2:76; A5: sup I in I by A3, XXREAL_2:def_6; thus ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by A5, A4, Def5; ::_thesis: verum end; supposeA6: ( I is left_end & not I is right_end ) ; ::_thesis: ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) set a = inf I; set b = sup I; A7: I = [.(inf I),(sup I).[ by A6, XXREAL_2:77; A8: inf I in I by A6, XXREAL_2:def_5; thus ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by A8, A7, Def4; ::_thesis: verum end; suppose ( not I is left_end & not I is right_end ) ; ::_thesis: ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) then consider a, b being ext-real number such that A9: a <= b and A10: I = ].a,b.[ by XXREAL_2:79; reconsider a = a, b = b as R_eal by XXREAL_0:def_1; a <= b by A9; hence ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by A10, Def2; ::_thesis: verum end; end; end; 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 ) proof let a, b be R_eal; ::_thesis: ( a < b implies ex x being R_eal st ( a < x & x < b & x in REAL ) ) 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 ; ::_thesis: ex x being R_eal st ( a < x & x < b & x in REAL ) then A4: ( not a = +infty & not b = -infty ) by XXREAL_0:4, XXREAL_0:6; percases ( ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) ) by A1, A2, A4, TARSKI:def_2; suppose ( a in REAL & b in REAL ) ; ::_thesis: ex x being R_eal st ( a < x & x < b & x in REAL ) then consider x, y being Real such that A5: ( x = a & y = b ) and x <= y by A3; consider z being real number such that A6: ( x < z & z < y ) by A3, A5, XREAL_1:5; reconsider z = z as Real by XREAL_0:def_1; reconsider o = z as R_eal by XXREAL_0:def_1; take o ; ::_thesis: ( a < o & o < b & o in REAL ) thus ( a < o & o < b & o in REAL ) by A5, A6; ::_thesis: verum end; supposeA7: ( a in REAL & b = +infty ) ; ::_thesis: ex x being R_eal st ( a < x & x < b & x in REAL ) then reconsider x = a as Real ; consider z being real number such that A8: x < z by XREAL_1:1; reconsider z = z as Real by XREAL_0:def_1; reconsider o = z as R_eal by XXREAL_0:def_1; take o ; ::_thesis: ( a < o & o < b & o in REAL ) thus ( a < o & o < b & o in REAL ) by A7, A8, XXREAL_0:9; ::_thesis: verum end; supposeA9: ( a = -infty & b in REAL ) ; ::_thesis: ex x being R_eal st ( a < x & x < b & x in REAL ) then reconsider y = b as Real ; consider z being real number such that A10: z < y by XREAL_1:2; reconsider z = z as Real by XREAL_0:def_1; reconsider o = z as R_eal by XXREAL_0:def_1; take o ; ::_thesis: ( a < o & o < b & o in REAL ) thus ( a < o & o < b & o in REAL ) by A9, A10, XXREAL_0:12; ::_thesis: verum end; supposeA11: ( a = -infty & b = +infty ) ; ::_thesis: ex x being R_eal st ( a < x & x < b & x in REAL ) take 0. ; ::_thesis: ( a < 0. & 0. < b & 0. in REAL ) 0. = 0 ; hence ( a < 0. & 0. < b & 0. in REAL ) by A11; ::_thesis: verum end; end; end; 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 ) proof let a, b, c be R_eal; ::_thesis: ( a < b & a < c implies ex x being R_eal st ( a < x & x < b & x < c & x in REAL ) ) A1: min (b,c) = min {b,c} by XXREAL_2:14; ex o being R_eal st ( o in {b,c} & o <= c ) proof take c ; ::_thesis: ( c in {b,c} & c <= c ) thus ( c in {b,c} & c <= c ) by TARSKI:def_2; ::_thesis: verum end; then A2: min (b,c) <= c by A1, XXREAL_2:62; reconsider m = min (b,c) as R_eal by XXREAL_0:def_1; assume ( a < b & a < c ) ; ::_thesis: ex x being R_eal st ( a < x & x < b & x < c & x in REAL ) then a < min (b,c) by XXREAL_0:def_9; then consider x being R_eal such that A3: ( a < x & x < m & x in REAL ) by Th2; take x ; ::_thesis: ( a < x & x < b & x < c & x in REAL ) ex o being R_eal st ( o in {b,c} & o <= b ) proof take b ; ::_thesis: ( b in {b,c} & b <= b ) thus ( b in {b,c} & b <= b ) by TARSKI:def_2; ::_thesis: verum end; then min (b,c) <= b by A1, XXREAL_2:62; hence ( a < x & x < b & x < c & x in REAL ) by A3, A2, XXREAL_0:2; ::_thesis: verum end; 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 ) proof let a, b, c be R_eal; ::_thesis: ( a < c & b < c implies ex x being R_eal st ( a < x & b < x & x < c & x in REAL ) ) reconsider m = max (a,b) as R_eal by XXREAL_0:def_1; A1: b in {a,b} by TARSKI:def_2; assume ( a < c & b < c ) ; ::_thesis: ex x being R_eal st ( a < x & b < x & x < c & x in REAL ) then max (a,b) < c by XXREAL_0:def_10; then consider x being R_eal such that A2: ( m < x & x < c & x in REAL ) by Th2; take x ; ::_thesis: ( a < x & b < x & x < c & x in REAL ) ( max (a,b) = max {a,b} & a in {a,b} ) by TARSKI:def_2, XXREAL_2:12; hence ( a < x & b < x & x < c & x in REAL ) by A2, A1, XXREAL_2:61; ::_thesis: verum end; 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. ) ) proof let a, b be R_eal; ::_thesis: ( ( a < b implies diameter ].a,b.[ = b - a ) & ( b <= a implies diameter ].a,b.[ = 0. ) ) hereby ::_thesis: ( b <= a implies diameter ].a,b.[ = 0. ) assume A1: a < b ; ::_thesis: diameter ].a,b.[ = b - a 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; ::_thesis: verum end; assume b <= a ; ::_thesis: diameter ].a,b.[ = 0. then ].a,b.[ = {} by XXREAL_1:28; hence diameter ].a,b.[ = 0. by Def6; ::_thesis: verum end; 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. ) ) proof let a, b be R_eal; ::_thesis: ( ( a <= b implies diameter [.a,b.] = b - a ) & ( b < a implies diameter [.a,b.] = 0. ) ) hereby ::_thesis: ( b < a implies diameter [.a,b.] = 0. ) assume A1: a <= b ; ::_thesis: diameter [.a,b.] = b - a 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; ::_thesis: verum end; assume b < a ; ::_thesis: diameter [.a,b.] = 0. then [.a,b.] = {} by XXREAL_1:29; hence diameter [.a,b.] = 0. by Def6; ::_thesis: verum end; 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. ) ) proof let a, b be R_eal; ::_thesis: ( ( a < b implies diameter [.a,b.[ = b - a ) & ( b <= a implies diameter [.a,b.[ = 0. ) ) hereby ::_thesis: ( b <= a implies diameter [.a,b.[ = 0. ) assume A1: a < b ; ::_thesis: diameter [.a,b.[ = b - a 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; ::_thesis: verum end; assume b <= a ; ::_thesis: diameter [.a,b.[ = 0. then [.a,b.[ = {} by XXREAL_1:27; hence diameter [.a,b.[ = 0. by Def6; ::_thesis: verum end; 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. ) ) proof let a, b be R_eal; ::_thesis: ( ( a < b implies diameter ].a,b.] = b - a ) & ( b <= a implies diameter ].a,b.] = 0. ) ) hereby ::_thesis: ( b <= a implies diameter ].a,b.] = 0. ) assume A1: a < b ; ::_thesis: diameter ].a,b.] = b - a 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; ::_thesis: verum end; assume b <= a ; ::_thesis: diameter ].a,b.] = 0. then ].a,b.] = {} by XXREAL_1:26; hence diameter ].a,b.] = 0. by Def6; ::_thesis: verum end; 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 proof let A be Interval; ::_thesis: 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 let a, b be R_eal; ::_thesis: ( a = -infty & b = +infty & ( A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.] ) implies diameter A = +infty ) assume that A1: ( a = -infty & b = +infty ) and A2: ( A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.] ) ; ::_thesis: diameter A = +infty A3: ( sup A = +infty & inf A = -infty ) by A1, A2, XXREAL_2:25, XXREAL_2:26, XXREAL_2:27, XXREAL_2:28, XXREAL_2:29, XXREAL_2:30, XXREAL_2:31, XXREAL_2:32; then not A is empty by XXREAL_2:40; then diameter A = b - a by A1, A3, Def6 .= +infty by A1, XXREAL_3:13 ; hence diameter A = +infty ; ::_thesis: verum end; 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 proof let S be Subset of REAL; ::_thesis: ( S is empty implies S is open_interval ) assume S is empty ; ::_thesis: S is open_interval then S = ].0.,0..[ ; hence S is open_interval by Def2; ::_thesis: verum end; end; theorem :: MEASURE5:10 diameter {} = 0. by Def6; Lm1: for A being Interval holds diameter A >= 0 proof let A be Interval; ::_thesis: diameter A >= 0 percases ( A is empty or not A is empty ) ; suppose A is empty ; ::_thesis: diameter A >= 0 hence diameter A >= 0 by Def6; ::_thesis: verum end; suppose not A is empty ; ::_thesis: diameter A >= 0 then inf A <= sup A by XXREAL_2:40; then (sup A) - (inf A) >= 0 by XXREAL_3:40; hence diameter A >= 0 by Def6; ::_thesis: verum end; end; end; Lm2: for A, B being Interval st A c= B holds diameter A <= diameter B proof let A, B be Interval; ::_thesis: ( A c= B implies diameter A <= diameter B ) assume A1: A c= B ; ::_thesis: diameter A <= diameter B percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: diameter A <= diameter B then diameter A = 0 by Def6; hence diameter A <= diameter B by Lm1; ::_thesis: verum end; supposeA2: A <> {} ; ::_thesis: diameter A <= diameter B 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, XXREAL_2:60; diameter A = (sup A) - (inf A) by A2, Def6; hence diameter A <= diameter B by A3, A4, XXREAL_3:37; ::_thesis: verum end; end; end; 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. ) proof let a, b be R_eal; ::_thesis: for A, B being Interval st A c= B & B = [.a,b.] & b <= a holds ( diameter A = 0. & diameter B = 0. ) let A, B be Interval; ::_thesis: ( A c= B & B = [.a,b.] & b <= a implies ( diameter A = 0. & diameter B = 0. ) ) assume that A1: A c= B and A2: B = [.a,b.] and A3: b <= a ; ::_thesis: ( diameter A = 0. & diameter B = 0. ) percases ( a = b or b < a ) by A3, XXREAL_0:1; supposeA4: a = b ; ::_thesis: ( diameter A = 0. & diameter B = 0. ) then B = {a} by A2, XXREAL_1:17; then ( inf B = a & sup B = a ) by XXREAL_2:11, XXREAL_2:13; then A5: diameter B = a - a by A2, A4, Def6 .= 0 by XXREAL_3:7 ; then diameter A <= 0 by A1, Lm2; hence ( diameter A = 0. & diameter B = 0. ) by A5, Lm1; ::_thesis: verum end; suppose b < a ; ::_thesis: ( diameter A = 0. & diameter B = 0. ) then A6: B = {} by A2, XXREAL_1:29; then A = {} by A1; hence ( diameter A = 0. & diameter B = 0. ) by A6, Def6; ::_thesis: verum end; end; end; 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.] ) ) proof let X be Subset of REAL; ::_thesis: ( ( not X is empty & X is closed_interval ) iff ex a, b being Real st ( a <= b & X = [.a,b.] ) ) thus ( not X is empty & X is closed_interval implies ex a, b being Real st ( a <= b & X = [.a,b.] ) ) ::_thesis: ( ex a, b being Real st ( a <= b & X = [.a,b.] ) implies ( not X is empty & X is closed_interval ) ) proof assume A1: not X is empty ; ::_thesis: ( not X is closed_interval or ex a, b being Real st ( a <= b & X = [.a,b.] ) ) assume X is closed_interval ; ::_thesis: ex a, b being Real st ( a <= b & X = [.a,b.] ) then consider a, b being real number such that A2: X = [.a,b.] by Def3; reconsider a = a, b = b as Real by XREAL_0:def_1; take a ; ::_thesis: ex b being Real st ( a <= b & X = [.a,b.] ) take b ; ::_thesis: ( a <= b & X = [.a,b.] ) thus a <= b by A1, A2, XXREAL_1:29; ::_thesis: X = [.a,b.] thus X = [.a,b.] by A2; ::_thesis: verum end; thus ( ex a, b being Real st ( a <= b & X = [.a,b.] ) implies ( not X is empty & X is closed_interval ) ) by Def3, XXREAL_1:30; ::_thesis: verum end;