let I be Element of Family_of_Intervals ; ( I <> {} & I is right_open_interval implies OS_Meas . I <= diameter I )
assume that
A1:
I <> {}
and
A2:
I is right_open_interval
; OS_Meas . I <= diameter I
consider a being Real, b being R_eal such that
A3:
I = [.a,b.[
by A2, MEASURE5:def 4;
A4:
a < b
by A1, A3, XXREAL_1:27;
reconsider a1 = a as R_eal by XXREAL_0:def 1;
per cases
( b = +infty or b <> +infty )
;
suppose A5:
b <> +infty
;
OS_Meas . I <= diameter I
-infty < a
by XXREAL_0:12, XREAL_0:def 1;
then
b in REAL
by A4, A5, XXREAL_0:14;
then reconsider rb =
b as
Real ;
A6:
diameter I =
b - a1
by A1, A3, XXREAL_1:27, MEASURE5:7
.=
rb - a
by Lm9
;
then reconsider DI =
diameter I as
Real ;
A7:
for
e being
Real st
0 < e holds
OS_Meas . I <= DI + e
proof
let e be
Real;
( 0 < e implies OS_Meas . I <= DI + e )
assume A8:
0 < e
;
OS_Meas . I <= DI + e
reconsider c =
a - e as
R_eal by XXREAL_0:def 1;
reconsider J =
].c,b.[ as
Subset of
REAL ;
A9:
J in Family_of_Intervals
by MEASUR10:def 1;
J is
open_interval
by MEASURE5:def 2;
then consider F being
Open_Interval_Covering of
J such that A10:
(
F . 0 = J & ( for
n being
Nat st
n <> 0 holds
F . n = {} ) &
union (rng F) = J &
SUM (F vol) = diameter J )
by A9, Th36;
A11:
c < a
by A8, XREAL_1:44;
then reconsider F1 =
F as
Open_Interval_Covering of
I by A3, Th38, XXREAL_1:48;
F vol = F1 vol
by Th39;
then
vol F1 = diameter J
by A10, MEASURE7:def 6;
then A12:
diameter J in Svc2 I
by Def7;
inf (Svc2 I) is
LowerBound of
Svc2 I
by XXREAL_2:def 4;
then A13:
inf (Svc2 I) <= diameter J
by A12, XXREAL_2:def 2;
inf (Svc I) <= inf (Svc2 I)
by Th30;
then A14:
inf (Svc I) <= diameter J
by A13, XXREAL_0:2;
c < b
by A1, A3, XXREAL_1:27, A11, XXREAL_0:2;
then
diameter J = b - c
by MEASURE5:5;
then
diameter J = rb - (a - e)
by Lm9;
hence
OS_Meas . I <= DI + e
by A6, A14, MEASURE7:def 10;
verum
end; then A15:
OS_Meas . I <= DI + 1
;
A16:
(
0 in REAL &
DI + 1
in REAL )
by XREAL_0:def 1;
OS_Meas is
V115()
by MEASURE4:def 1;
then
0 <= OS_Meas . I
by SUPINF_2:51;
then
OS_Meas . I in REAL
by A15, A16, XXREAL_0:45;
then reconsider LI =
OS_Meas . I as
Real ;
for
e being
Real st
0 < e holds
LI <= DI + e
by A7;
hence
OS_Meas . I <= diameter I
by XREAL_1:41;
verum end;