let I be Element of Family_of_Intervals ; ( not I is empty & I is right_open_interval & diameter I < +infty implies diameter I <= OS_Meas . I )
assume that
A1:
( not I is empty & I is right_open_interval )
and
A2:
diameter I < +infty
; diameter I <= OS_Meas . I
0 <= diameter I
by A1, MEASURE5:13;
then
diameter I in REAL
by A2, XXREAL_0:14;
then reconsider DI = diameter I as Real ;
A3:
OS_Meas . I <= diameter I
by A1, Th44;
OS_Meas is V115()
by MEASURE4:def 1;
then
( -infty < 0 & 0 <= OS_Meas . I )
by SUPINF_2:51;
then
OS_Meas . I in REAL
by A2, A3, XXREAL_0:14;
then reconsider LI = OS_Meas . I as Real ;
consider r1 being Real, a2 being R_eal such that
A4:
I = [.r1,a2.[
by A1, MEASURE5:def 4;
reconsider a1 = r1 as R_eal by XXREAL_0:def 1;
a2 <> -infty
by A1, A4, XXREAL_1:27, XXREAL_0:5;
then
a2 in REAL
by A5, XXREAL_0:14;
then reconsider r2 = a2 as Real ;
DI = a2 - a1
by A1, A4, XXREAL_1:27, MEASURE5:7;
then A6:
DI = r2 - r1
by Lm9;
then
0 < DI
by A1, A4, XXREAL_1:27, XREAL_1:50;
then A7:
( DI / 2 < DI & 0 < DI / 2 )
by XREAL_1:215, XREAL_1:216;
for e being Real st 0 < e holds
DI <= LI + e
proof
let e be
Real;
( 0 < e implies DI <= LI + e )
assume A8:
0 < e
;
DI <= LI + e
set e1 =
min (
(DI / 2),
e);
A9:
min (
(DI / 2),
e)
> 0
by A7, A8, XXREAL_0:21;
(
min (
(DI / 2),
e)
<= DI / 2 &
min (
(DI / 2),
e)
<= e )
by XXREAL_0:17;
then A10:
min (
(DI / 2),
e)
< DI
by A7, XXREAL_0:2;
set J =
[.(r1 + ((min ((DI / 2),e)) / 2)),(r2 - ((min ((DI / 2),e)) / 2)).];
(r2 - ((min ((DI / 2),e)) / 2)) - (r1 + ((min ((DI / 2),e)) / 2)) = DI - (min ((DI / 2),e))
by A6;
then
(r2 - ((min ((DI / 2),e)) / 2)) - (r1 + ((min ((DI / 2),e)) / 2)) > 0
by A10, XREAL_1:50;
then A11:
r1 + ((min ((DI / 2),e)) / 2) < r2 - ((min ((DI / 2),e)) / 2)
by XREAL_1:47;
then reconsider J =
[.(r1 + ((min ((DI / 2),e)) / 2)),(r2 - ((min ((DI / 2),e)) / 2)).] as non
empty closed_interval Subset of
REAL by MEASURE5:14;
reconsider j1 =
r1 + ((min ((DI / 2),e)) / 2),
j2 =
r2 - ((min ((DI / 2),e)) / 2) as
R_eal by XXREAL_0:def 1;
A12:
diameter J = j2 - j1
by A11, MEASURE5:6;
then reconsider DJ =
diameter J as
Real ;
diameter J = (r2 - ((min ((DI / 2),e)) / 2)) - (r1 + ((min ((DI / 2),e)) / 2))
by A12, Lm9;
then
DI = DJ + (min ((DI / 2),e))
by A6;
then A13:
DI <= DJ + e
by XXREAL_0:17, XREAL_1:6;
J in { I where I is Interval : verum }
;
then A14:
diameter J <= OS_Meas . J
by Lm14, MEASUR10:def 1;
(
r1 < r1 + ((min ((DI / 2),e)) / 2) &
r2 - ((min ((DI / 2),e)) / 2) < r2 )
by A9, XREAL_1:29, XREAL_1:44, XREAL_1:215;
then
J c= I
by A4, XXREAL_1:43;
then
OS_Meas . J <= LI
by MEASURE4:def 1;
then
DJ <= LI
by A14, XXREAL_0:2;
then
DJ + e <= LI + e
by XREAL_1:6;
hence
DI <= LI + e
by A13, XXREAL_0:2;
verum
end;
hence
diameter I <= OS_Meas . I
by XREAL_1:41; verum