let I be Element of Family_of_Intervals ; ( I <> {} & I is closed_interval implies OS_Meas . I <= diameter I )
assume that
A1:
I <> {}
and
A2:
I is closed_interval
; OS_Meas . I <= diameter I
consider a, b being Real such that
A3:
I = [.a,b.]
by A2, MEASURE5:def 3;
reconsider a1 = a, b1 = b as R_eal by XXREAL_0:def 1;
A4:
diameter I = b1 - a1
by A1, A3, XXREAL_1:29, MEASURE5:6;
then A5:
diameter I = b - a
by Lm9;
reconsider DI = diameter I as Real by A4;
A6:
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
0 < e
;
OS_Meas . I <= DI + e
then A7:
(
a - (e / 2) < a &
b < b + (e / 2) )
by XREAL_1:29, XREAL_1:44, XREAL_1:215;
reconsider p =
a - (e / 2),
q =
b + (e / 2) as
R_eal by XXREAL_0:def 1;
reconsider J =
].p,q.[ as
Subset of
REAL ;
A8:
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 A9:
(
F . 0 = J & ( for
n being
Nat st
n <> 0 holds
F . n = {} ) &
union (rng F) = J &
SUM (F vol) = diameter J )
by A8, Th36;
reconsider F1 =
F as
Open_Interval_Covering of
I by A3, A7, Th38, XXREAL_1:47;
a <= b
by A1, A3, XXREAL_1:29;
then
a - (e / 2) < b
by A7, XXREAL_0:2;
then
a - (e / 2) < b + (e / 2)
by A7, XXREAL_0:2;
then
diameter J = q - p
by MEASURE5:5;
then A10:
diameter J = (b + (e / 2)) - (a - (e / 2))
by Lm9;
F vol = F1 vol
by Th39;
then
vol F1 = diameter J
by A9, MEASURE7:def 6;
then A11:
diameter J in Svc2 I
by Def7;
inf (Svc2 I) is
LowerBound of
Svc2 I
by XXREAL_2:def 4;
then A12:
inf (Svc2 I) <= diameter J
by A11, XXREAL_2:def 2;
inf (Svc I) <= inf (Svc2 I)
by Th30;
then
inf (Svc I) <= diameter J
by A12, XXREAL_0:2;
hence
OS_Meas . I <= DI + e
by A5, A10, MEASURE7:def 10;
verum
end;
then A13:
OS_Meas . I <= DI + 1
;
A14:
( 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 A14, A13, XXREAL_0:45;
then reconsider LI = OS_Meas . I as Real ;
for e being Real st 0 < e holds
LI <= DI + e
by A6;
hence
OS_Meas . I <= diameter I
by XREAL_1:41; verum