:: MEASURE5 semantic presentation
begin
scheme
:: MEASURE5:sch 1
RSetEq
{
P
1
[ ( ( ) ( )
set
) ] } :
for
X1
,
X2
being ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) st ( for
x
being ( ( ) (
ext-real
)
R_eal
) holds
(
x
: ( ( ) (
ext-real
)
R_eal
)
in
X1
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) iff
P
1
[
x
: ( ( ) (
ext-real
)
R_eal
) ] ) ) & ( for
x
being ( ( ) (
ext-real
)
R_eal
) holds
(
x
: ( ( ) (
ext-real
)
R_eal
)
in
X2
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) iff
P
1
[
x
: ( ( ) (
ext-real
)
R_eal
) ] ) ) holds
X1
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
=
X2
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
proof
end;
definition
let
a
,
b
be ( ( ) (
ext-real
)
R_eal
) ;
:: original:
].
redefine
func
].
a
,
b
.[
->
( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
means
:: MEASURE5:def 1
for
x
being ( ( ) (
ext-real
)
R_eal
) holds
(
x
: ( ( ) (
ext-real
)
R_eal
)
in
it
: ( (
V12
()
V33
(
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
V12
()
V33
(
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ,
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) )
Num
of
a
: ( ( ) (
ext-real
)
R_eal
) ) ) ) (
V12
()
V33
(
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
V12
()
V33
(
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ,
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) )
Num
of
a
: ( ( ) (
ext-real
)
R_eal
) ) ) )
Element
of
K32
(
K33
(
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
V12
()
V33
(
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ,
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) )
Num
of
a
: ( ( ) (
ext-real
)
R_eal
) ) ) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) iff (
a
: ( ( ) (
ext-real
)
R_eal
)
<
x
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
<
b
: ( ( ) (
V12
()
V33
(
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ,
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) )
Num
of
a
: ( ( ) (
ext-real
)
R_eal
) ) ) );
end;
definition
let
IT
be ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
open_interval
means
:: MEASURE5:def 2
ex
a
,
b
being ( ( ) (
ext-real
)
R_eal
) st
IT
: ( ( ) (
ext-real
)
R_eal
)
=
].
a
: ( (
real
) (
V24
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V24
()
real
ext-real
)
number
)
.[
: ( ( ) (
complex-membered
ext-real-membered
real-membered
non
left_end
non
right_end
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
closed_interval
means
:: MEASURE5:def 3
ex
a
,
b
being ( (
real
) (
V24
()
real
ext-real
)
number
) st
IT
: ( ( ) (
ext-real
)
R_eal
)
=
[.
a
: ( (
real
) (
V24
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V24
()
real
ext-real
)
number
)
.]
: ( ( ) (
complex-membered
ext-real-membered
real-membered
interval
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
cluster
non
empty
complex-membered
ext-real-membered
real-membered
open_interval
for ( ( ) ( )
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
cluster
non
empty
complex-membered
ext-real-membered
real-membered
closed_interval
for ( ( ) ( )
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
IT
be ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
right_open_interval
means
:: MEASURE5:def 4
ex
a
being ( (
real
) (
V24
()
real
ext-real
)
number
) ex
b
being ( ( ) (
ext-real
)
R_eal
) st
IT
: ( ( ) (
ext-real
)
R_eal
)
=
[.
a
: ( (
real
) (
V24
()
real
ext-real
)
number
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.[
: ( ( ) (
complex-membered
ext-real-membered
real-membered
non
right_end
interval
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
notation
let
IT
be ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
synonym
left_closed_interval
IT
for
right_open_interval
;
end;
definition
let
IT
be ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
left_open_interval
means
:: MEASURE5:def 5
ex
a
being ( ( ) (
ext-real
)
R_eal
) ex
b
being ( (
real
) (
V24
()
real
ext-real
)
number
) st
IT
: ( ( ) (
ext-real
)
R_eal
)
=
].
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( (
real
) (
V24
()
real
ext-real
)
number
)
.]
: ( ( ) (
complex-membered
ext-real-membered
real-membered
non
left_end
interval
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
notation
let
IT
be ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
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
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
cluster
non
empty
complex-membered
ext-real-membered
real-membered
left_open_interval
for ( ( ) ( )
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
mode
Interval
is
( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
end;
registration
cluster
open_interval
->
interval
for ( ( ) ( )
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
cluster
closed_interval
->
interval
for ( ( ) ( )
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
cluster
right_open_interval
->
interval
for ( ( ) ( )
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
cluster
left_open_interval
->
interval
for ( ( ) ( )
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: MEASURE5:1
for
I
being ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
(
I
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
open_interval
or
I
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
closed_interval
or
I
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
right_open_interval
or
I
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
left_open_interval
) ;
theorem
:: MEASURE5:2
for
a
,
b
being ( ( ) (
ext-real
)
R_eal
) st
a
: ( ( ) (
ext-real
)
R_eal
)
<
b
: ( ( ) (
ext-real
)
R_eal
) holds
ex
x
being ( ( ) (
ext-real
)
R_eal
) st
(
a
: ( ( ) (
ext-real
)
R_eal
)
<
x
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
<
b
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
in
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) ;
theorem
:: MEASURE5:3
for
a
,
b
,
c
being ( ( ) (
ext-real
)
R_eal
) st
a
: ( ( ) (
ext-real
)
R_eal
)
<
b
: ( ( ) (
ext-real
)
R_eal
) &
a
: ( ( ) (
ext-real
)
R_eal
)
<
c
: ( ( ) (
ext-real
)
R_eal
) holds
ex
x
being ( ( ) (
ext-real
)
R_eal
) st
(
a
: ( ( ) (
ext-real
)
R_eal
)
<
x
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
<
b
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
<
c
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
in
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) ;
theorem
:: MEASURE5:4
for
a
,
b
,
c
being ( ( ) (
ext-real
)
R_eal
) st
a
: ( ( ) (
ext-real
)
R_eal
)
<
c
: ( ( ) (
ext-real
)
R_eal
) &
b
: ( ( ) (
ext-real
)
R_eal
)
<
c
: ( ( ) (
ext-real
)
R_eal
) holds
ex
x
being ( ( ) (
ext-real
)
R_eal
) st
(
a
: ( ( ) (
ext-real
)
R_eal
)
<
x
: ( ( ) (
ext-real
)
R_eal
) &
b
: ( ( ) (
ext-real
)
R_eal
)
<
x
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
<
c
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
in
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) ;
definition
let
A
be ( (
ext-real-membered
) (
ext-real-membered
)
set
) ;
func
diameter
A
->
( ( ) (
ext-real
)
R_eal
)
equals
:: MEASURE5:def 6
(
sup
A
: ( (
V5
() ) (
V5
() )
set
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
-
(
inf
A
: ( (
V5
() ) (
V5
() )
set
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
if
A
: ( (
V5
() ) (
V5
() )
set
)
<>
{}
: ( ( ) (
empty
V36
()
V40
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
bounded_above
real-bounded
interval
)
set
)
otherwise
0.
: ( ( ) (
empty
ext-real
non
positive
non
negative
V36
()
V40
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
bounded_above
real-bounded
interval
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ;
end;
theorem
:: MEASURE5:5
for
a
,
b
being ( ( ) (
ext-real
)
R_eal
) holds
( (
a
: ( ( ) (
ext-real
)
R_eal
)
<
b
: ( ( ) (
ext-real
)
R_eal
) implies
diameter
].
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.[
: ( ( ) (
complex-membered
ext-real-membered
real-membered
non
left_end
non
right_end
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
)
R_eal
)
=
b
: ( ( ) (
ext-real
)
R_eal
)
-
a
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) & (
b
: ( ( ) (
ext-real
)
R_eal
)
<=
a
: ( ( ) (
ext-real
)
R_eal
) implies
diameter
].
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.[
: ( ( ) (
complex-membered
ext-real-membered
real-membered
non
left_end
non
right_end
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
)
R_eal
)
=
0.
: ( ( ) (
empty
ext-real
non
positive
non
negative
V36
()
V40
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
bounded_above
real-bounded
interval
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) ) ;
theorem
:: MEASURE5:6
for
a
,
b
being ( ( ) (
ext-real
)
R_eal
) holds
( (
a
: ( ( ) (
ext-real
)
R_eal
)
<=
b
: ( ( ) (
ext-real
)
R_eal
) implies
diameter
[.
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.]
: ( ( ) (
ext-real-membered
interval
)
set
) : ( ( ) (
ext-real
)
R_eal
)
=
b
: ( ( ) (
ext-real
)
R_eal
)
-
a
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) & (
b
: ( ( ) (
ext-real
)
R_eal
)
<
a
: ( ( ) (
ext-real
)
R_eal
) implies
diameter
[.
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.]
: ( ( ) (
ext-real-membered
interval
)
set
) : ( ( ) (
ext-real
)
R_eal
)
=
0.
: ( ( ) (
empty
ext-real
non
positive
non
negative
V36
()
V40
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
bounded_above
real-bounded
interval
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) ) ;
theorem
:: MEASURE5:7
for
a
,
b
being ( ( ) (
ext-real
)
R_eal
) holds
( (
a
: ( ( ) (
ext-real
)
R_eal
)
<
b
: ( ( ) (
ext-real
)
R_eal
) implies
diameter
[.
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.[
: ( ( ) (
ext-real-membered
non
right_end
interval
)
set
) : ( ( ) (
ext-real
)
R_eal
)
=
b
: ( ( ) (
ext-real
)
R_eal
)
-
a
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) & (
b
: ( ( ) (
ext-real
)
R_eal
)
<=
a
: ( ( ) (
ext-real
)
R_eal
) implies
diameter
[.
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.[
: ( ( ) (
ext-real-membered
non
right_end
interval
)
set
) : ( ( ) (
ext-real
)
R_eal
)
=
0.
: ( ( ) (
empty
ext-real
non
positive
non
negative
V36
()
V40
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
bounded_above
real-bounded
interval
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) ) ;
theorem
:: MEASURE5:8
for
a
,
b
being ( ( ) (
ext-real
)
R_eal
) holds
( (
a
: ( ( ) (
ext-real
)
R_eal
)
<
b
: ( ( ) (
ext-real
)
R_eal
) implies
diameter
].
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.]
: ( ( ) (
ext-real-membered
non
left_end
interval
)
set
) : ( ( ) (
ext-real
)
R_eal
)
=
b
: ( ( ) (
ext-real
)
R_eal
)
-
a
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) & (
b
: ( ( ) (
ext-real
)
R_eal
)
<=
a
: ( ( ) (
ext-real
)
R_eal
) implies
diameter
].
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.]
: ( ( ) (
ext-real-membered
non
left_end
interval
)
set
) : ( ( ) (
ext-real
)
R_eal
)
=
0.
: ( ( ) (
empty
ext-real
non
positive
non
negative
V36
()
V40
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
bounded_above
real-bounded
interval
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) ) ;
theorem
:: MEASURE5:9
for
A
being ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
a
,
b
being ( ( ) (
ext-real
)
R_eal
) st
a
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) ( non
empty
non
real
ext-real
non
positive
negative
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) &
b
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) ( non
empty
non
real
ext-real
positive
non
negative
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) & (
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
].
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.[
: ( ( ) (
complex-membered
ext-real-membered
real-membered
non
left_end
non
right_end
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) or
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
[.
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.]
: ( ( ) (
ext-real-membered
interval
)
set
) or
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
[.
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.[
: ( ( ) (
ext-real-membered
non
right_end
interval
)
set
) or
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
].
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.]
: ( ( ) (
ext-real-membered
non
left_end
interval
)
set
) ) holds
diameter
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) ( non
empty
non
real
ext-real
positive
non
negative
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ;
registration
cluster
empty
->
open_interval
for ( ( ) ( )
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: MEASURE5:10
diameter
{}
: ( ( ) (
empty
V36
()
V40
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
bounded_above
real-bounded
interval
)
set
) : ( ( ) (
ext-real
)
R_eal
)
=
0.
: ( ( ) (
empty
ext-real
non
positive
non
negative
V36
()
V40
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
bounded_above
real-bounded
interval
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ;
theorem
:: MEASURE5:11
for
a
,
b
being ( ( ) (
ext-real
)
R_eal
)
for
A
,
B
being ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) st
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
c=
B
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) &
B
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
[.
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.]
: ( ( ) (
ext-real-membered
interval
)
set
) &
b
: ( ( ) (
ext-real
)
R_eal
)
<=
a
: ( ( ) (
ext-real
)
R_eal
) holds
(
diameter
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
R_eal
)
=
0.
: ( ( ) (
empty
ext-real
non
positive
non
negative
V36
()
V40
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
bounded_above
real-bounded
interval
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) &
diameter
B
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
R_eal
)
=
0.
: ( ( ) (
empty
ext-real
non
positive
non
negative
V36
()
V40
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
bounded_above
real-bounded
interval
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) ;
theorem
:: MEASURE5:12
for
A
,
B
being ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) st
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
c=
B
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) holds
diameter
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
R_eal
)
<=
diameter
B
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
R_eal
) ;
theorem
:: MEASURE5:13
for
A
being ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) holds
0.
: ( ( ) (
empty
ext-real
non
positive
non
negative
V36
()
V40
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V47
()
bounded_below
bounded_above
real-bounded
interval
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
<=
diameter
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
R_eal
) ;
theorem
:: MEASURE5:14
for
X
being ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
( ( not
X
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
empty
&
X
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
closed_interval
) iff ex
a
,
b
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
(
a
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<=
b
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
X
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
=
[.
a
: ( ( ) (
V24
()
real
ext-real
)
Real
) ,
b
: ( ( ) (
V24
()
real
ext-real
)
Real
)
.]
: ( ( ) (
complex-membered
ext-real-membered
real-membered
interval
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V5
()
V36
()
complex-membered
ext-real-membered
real-membered
V47
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ) ;