:: Properties of the Intervals of Real Numbers
:: by J\'ozef Bia{\l}as
::
:: Received January 12, 1993
:: Copyright (c) 1993-2011 Association of Mizar Users


begin

theorem :: MEASURE5:1
canceled;

theorem :: MEASURE5:2
canceled;

theorem :: MEASURE5:3
canceled;

theorem :: MEASURE5:4
canceled;

theorem :: MEASURE5:5
canceled;

theorem :: MEASURE5:6
canceled;

theorem :: MEASURE5:7
canceled;

theorem :: MEASURE5:8
canceled;

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

definition
canceled;
let a, b be R_eal;
:: original: ].
redefine func ].a,b.[ -> Subset of REAL means :: MEASURE5:def 2
for x being R_eal holds
( x in it iff ( a < x & x < b ) );
coherence
].a,b.[ is Subset of REAL
proof 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 end;
end;

:: deftheorem MEASURE5:def 1 :
canceled;

:: deftheorem defines ]. MEASURE5:def 2 :
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
canceled;
canceled;
let IT be Subset of REAL;
attr IT is open_interval means :Def5: :: MEASURE5:def 5
ex a, b being R_eal st IT = ].a,b.[;
attr IT is closed_interval means :Def6: :: MEASURE5:def 6
ex a, b being real number st IT = [.a,b.];
end;

:: deftheorem MEASURE5:def 3 :
canceled;

:: deftheorem MEASURE5:def 4 :
canceled;

:: deftheorem Def5 defines open_interval MEASURE5:def 5 :
for IT being Subset of REAL holds
( IT is open_interval iff ex a, b being R_eal st IT = ].a,b.[ );

:: deftheorem Def6 defines closed_interval MEASURE5:def 6 :
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 Element of K18(REAL);
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is open_interval )
proof end;
cluster non empty complex-membered ext-real-membered real-membered closed_interval Element of K18(REAL);
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is closed_interval )
proof end;
end;

definition
let IT be Subset of REAL;
attr IT is right_open_interval means :Def7: :: MEASURE5:def 7
ex a being real number ex b being R_eal st IT = [.a,b.[;
end;

:: deftheorem Def7 defines right_open_interval MEASURE5:def 7 :
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;
attr IT is left_open_interval means :Def8: :: MEASURE5:def 8
ex a being R_eal ex b being real number st IT = ].a,b.];
end;

:: deftheorem Def8 defines left_open_interval MEASURE5:def 8 :
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 Element of K18(REAL);
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is right_open_interval )
proof end;
cluster non empty complex-membered ext-real-membered real-membered left_open_interval Element of K18(REAL);
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is left_open_interval )
proof end;
end;

definition
mode Interval is interval Subset of REAL;
end;

registration
cluster open_interval -> interval Element of K18(REAL);
coherence
for b1 being Subset of REAL st b1 is open_interval holds
b1 is interval
proof end;
cluster closed_interval -> interval Element of K18(REAL);
coherence
for b1 being Subset of REAL st b1 is closed_interval holds
b1 is interval
proof end;
cluster right_open_interval -> interval Element of K18(REAL);
coherence
for b1 being Subset of REAL st b1 is right_open_interval holds
b1 is interval
proof end;
cluster left_open_interval -> interval Element of K18(REAL);
coherence
for b1 being Subset of REAL st b1 is left_open_interval holds
b1 is interval
proof end;
end;

theorem :: MEASURE5:9
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 end;

theorem :: MEASURE5:10
canceled;

theorem :: MEASURE5:11
canceled;

theorem :: MEASURE5:12
canceled;

theorem :: MEASURE5:13
canceled;

theorem :: MEASURE5:14
canceled;

theorem :: MEASURE5:15
canceled;

theorem :: MEASURE5:16
canceled;

theorem Th17: :: MEASURE5:17
for a, b being R_eal st a < b holds
ex x being R_eal st
( a < x & x < b & x in REAL )
proof end;

theorem :: MEASURE5:18
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 end;

theorem :: MEASURE5:19
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 end;

definition
canceled;
let A be ext-real-membered set ;
func diameter A -> R_eal equals :Def10: :: MEASURE5:def 10
(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 MEASURE5:def 9 :
canceled;

:: deftheorem Def10 defines diameter MEASURE5:def 10 :
for A being ext-real-membered set holds
( ( A <> {} implies diameter A = (sup A) - (inf A) ) & ( not A <> {} implies diameter A = 0. ) );

theorem :: MEASURE5:20
canceled;

theorem :: MEASURE5:21
canceled;

theorem :: MEASURE5:22
canceled;

theorem :: MEASURE5:23
canceled;

theorem :: MEASURE5:24
canceled;

theorem :: MEASURE5:25
canceled;

theorem :: MEASURE5:26
canceled;

theorem :: MEASURE5:27
canceled;

theorem :: MEASURE5:28
canceled;

theorem :: MEASURE5:29
canceled;

theorem :: MEASURE5:30
canceled;

theorem :: MEASURE5:31
canceled;

theorem :: MEASURE5:32
canceled;

theorem :: MEASURE5:33
canceled;

theorem :: MEASURE5:34
canceled;

theorem :: MEASURE5:35
canceled;

theorem :: MEASURE5:36
canceled;

theorem :: MEASURE5:37
canceled;

theorem :: MEASURE5:38
canceled;

theorem :: MEASURE5:39
canceled;

theorem :: MEASURE5:40
canceled;

theorem :: MEASURE5:41
canceled;

theorem :: MEASURE5:42
canceled;

theorem :: MEASURE5:43
canceled;

theorem :: MEASURE5:44
canceled;

theorem :: MEASURE5:45
canceled;

theorem :: MEASURE5:46
canceled;

theorem :: MEASURE5:47
canceled;

theorem :: MEASURE5:48
canceled;

theorem :: MEASURE5:49
canceled;

theorem :: MEASURE5:50
canceled;

theorem :: MEASURE5:51
canceled;

theorem :: MEASURE5:52
canceled;

theorem :: MEASURE5:53
canceled;

theorem :: MEASURE5:54
for a, b being R_eal holds
( ( a < b implies diameter ].a,b.[ = b - a ) & ( b <= a implies diameter ].a,b.[ = 0. ) )
proof end;

theorem :: MEASURE5:55
for a, b being R_eal holds
( ( a <= b implies diameter [.a,b.] = b - a ) & ( b < a implies diameter [.a,b.] = 0. ) )
proof end;

theorem :: MEASURE5:56
for a, b being R_eal holds
( ( a < b implies diameter [.a,b.[ = b - a ) & ( b <= a implies diameter [.a,b.[ = 0. ) )
proof end;

theorem :: MEASURE5:57
for a, b being R_eal holds
( ( a < b implies diameter ].a,b.] = b - a ) & ( b <= a implies diameter ].a,b.] = 0. ) )
proof end;

theorem :: MEASURE5:58
canceled;

theorem :: MEASURE5:59
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 end;

registration
cluster empty -> open_interval Element of K18(REAL);
coherence
for b1 being Subset of REAL st b1 is empty holds
b1 is open_interval
proof end;
end;

theorem :: MEASURE5:60
diameter {} = 0. by Def10;

Lm1: for A being Interval holds diameter A >= 0
proof end;

Lm2: for A, B being Interval st A c= B holds
diameter A <= diameter B
proof end;

theorem :: MEASURE5:61
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 end;

theorem :: MEASURE5:62
for A, B being Interval st A c= B holds
diameter A <= diameter B by Lm2;

theorem :: MEASURE5:63
for A being Interval holds 0. <= diameter A by Lm1;