:: by J\'ozef Bia{\l}as

::

:: Received January 12, 1993

:: Copyright (c) 1993-2019 Association of Mizar Users

:: PROPERTIES OF THE INTERVALS

definition

let a, b be R_eal;

].a,b.[ is Subset of REAL

for b_{1} being Subset of REAL holds

( b_{1} = ].a,b.[ iff for x being R_eal holds

( x in b_{1} iff ( a < x & x < b ) ) )

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

].a,b.[ is Subset of REAL

proof end;

compatibility for b

( b

( x in b

proof end;

:: deftheorem defines ]. MEASURE5:def 1 :

for a, b being R_eal

for b_{3} being Subset of REAL holds

( b_{3} = ].a,b.[ iff for x being R_eal holds

( x in b_{3} iff ( a < x & x < b ) ) );

for a, b being R_eal

for b

( b

( x in b

:: deftheorem 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.[ );

for IT being Subset of REAL holds

( IT is open_interval iff ex a, b being R_eal st IT = ].a,b.[ );

:: deftheorem defines closed_interval MEASURE5:def 3 :

for IT being Subset of REAL holds

( IT is closed_interval iff ex a, b being Real st IT = [.a,b.] );

for IT being Subset of REAL holds

( IT is closed_interval iff ex a, b being Real st IT = [.a,b.] );

registration

ex b_{1} being Subset of REAL st

( not b_{1} is empty & b_{1} is open_interval )

ex b_{1} being Subset of REAL st

( not b_{1} is empty & b_{1} is closed_interval )
end;

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

existence ex b

( not b

proof end;

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

existence ex b

( not b

proof end;

definition

let IT be Subset of REAL;

end;
attr IT is right_open_interval means :: MEASURE5:def 4

ex a being Real ex b being R_eal st IT = [.a,b.[;

ex a being Real ex b being R_eal st IT = [.a,b.[;

:: deftheorem defines right_open_interval MEASURE5:def 4 :

for IT being Subset of REAL holds

( IT is right_open_interval iff ex a being Real ex b being R_eal st IT = [.a,b.[ );

for IT being Subset of REAL holds

( IT is right_open_interval iff ex a being Real ex b being R_eal st IT = [.a,b.[ );

definition

let IT be Subset of REAL;

end;
attr IT is left_open_interval means :: MEASURE5:def 5

ex a being R_eal ex b being Real st IT = ].a,b.];

ex a being R_eal ex b being Real st IT = ].a,b.];

:: deftheorem 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 st IT = ].a,b.] );

for IT being Subset of REAL holds

( IT is left_open_interval iff ex a being R_eal ex b being Real st IT = ].a,b.] );

registration

ex b_{1} being Subset of REAL st

( not b_{1} is empty & b_{1} is right_open_interval )

ex b_{1} being Subset of REAL st

( not b_{1} is empty & b_{1} is left_open_interval )
end;

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

existence ex b

( not b

proof end;

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

existence ex b

( not b

proof end;

registration

coherence

for b_{1} being Subset of REAL st b_{1} is open_interval holds

b_{1} is interval
;

coherence

for b_{1} being Subset of REAL st b_{1} is closed_interval holds

b_{1} is interval
;

coherence

for b_{1} being Subset of REAL st b_{1} is right_open_interval holds

b_{1} is interval
;

coherence

for b_{1} being Subset of REAL st b_{1} is left_open_interval holds

b_{1} is interval
;

end;
for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

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 )

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

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 )

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 ;

coherence

( ( A <> {} implies (sup A) - (inf A) is R_eal ) & ( not A <> {} implies 0. is R_eal ) ) ;

consistency

for b_{1} being R_eal holds verum
;

end;
coherence

( ( A <> {} implies (sup A) - (inf A) is R_eal ) & ( not A <> {} implies 0. is R_eal ) ) ;

consistency

for b

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

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

( ( 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. ) )

( ( 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. ) )

( ( 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. ) )

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

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

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

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: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.] ) ) by XXREAL_1:29, XXREAL_1:30;

( ( not X is empty & X is closed_interval ) iff ex a, b being Real st

( a <= b & X = [.a,b.] ) ) by XXREAL_1:29, XXREAL_1:30;