:: 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;