MEASURE5: Properties of the Intervals of Real Numbers

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

:: PROPERTIES OF THE INTERVALS

scheme :: MEASURE5:sch 1
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 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 ) );

proof end;

proof end;

end;

:: deftheorem defines ]. MEASURE5:def 1 :

definition

let IT be Subset of REAL;

attr IT is open_interval means :Def2: :: MEASURE5:def 2
ex a, b being R_eal st IT = ].a,b.[;

attr IT is closed_interval means :Def3: :: MEASURE5:def 3
ex a, b being Real st IT = [.a,b.];

end;

:: deftheorem Def2 defines open_interval MEASURE5:def 2 :

:: deftheorem Def3 defines closed_interval MEASURE5:def 3 :

registration

cluster non empty complex-membered ext-real-membered real-membered open_interval for Element of K32(REAL);

proof end;

cluster non empty complex-membered ext-real-membered real-membered closed_interval for Element of K32(REAL);

proof end;

end;

definition

let IT be Subset of REAL;

attr IT is right_open_interval means :Def4: :: MEASURE5:def 4
ex a being Real ex b being R_eal st IT = [.a,b.[;

end;

:: deftheorem Def4 defines right_open_interval MEASURE5:def 4 :

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 :Def5: :: MEASURE5:def 5
ex a being R_eal ex b being Real st IT = ].a,b.];

end;

:: deftheorem Def5 defines left_open_interval MEASURE5:def 5 :

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

proof end;

cluster non empty complex-membered ext-real-membered real-membered left_open_interval for Element of K32(REAL);

proof end;

end;

definition

mode Interval is interval Subset of REAL;

end;

registration

cluster open_interval -> interval for Element of K32(REAL);

proof end;

cluster closed_interval -> interval for Element of K32(REAL);

proof end;

cluster right_open_interval -> interval for Element of K32(REAL);

proof end;

cluster left_open_interval -> interval for Element of K32(REAL);

proof 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 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 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 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 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 ;
consistency ;

end;

:: deftheorem Def6 defines diameter MEASURE5:def 6 :

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

registration

cluster empty -> open_interval for Element of K32(REAL);

proof end;

end;

theorem :: MEASURE5:10

diameter {} = 0. by Def6;

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