let A be non empty closed_interval Subset of REAL; for F being FinSequence of bool REAL
for G being FinSequence of ExtREAL st A c= union (rng F) & len F = len G & ( for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL ) & ( for n being Nat st n in dom F holds
G . n = diameter (F . n) ) & ( for n being Nat st n in dom F holds
A meets F . n ) holds
diameter A <= Sum G
let F be FinSequence of bool REAL; for G being FinSequence of ExtREAL st A c= union (rng F) & len F = len G & ( for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL ) & ( for n being Nat st n in dom F holds
G . n = diameter (F . n) ) & ( for n being Nat st n in dom F holds
A meets F . n ) holds
diameter A <= Sum G
let G be FinSequence of ExtREAL ; ( A c= union (rng F) & len F = len G & ( for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL ) & ( for n being Nat st n in dom F holds
G . n = diameter (F . n) ) & ( for n being Nat st n in dom F holds
A meets F . n ) implies diameter A <= Sum G )
assume that
A1:
A c= union (rng F)
and
A2:
len F = len G
and
A3:
for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL
and
A4:
for n being Nat st n in dom F holds
G . n = diameter (F . n)
and
A5:
for n being Nat st n in dom F holds
A meets F . n
; diameter A <= Sum G
consider F1 being FinSequence of bool REAL such that
A6:
( F,F1 are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < len F1 holds
union (rng (F1 | n)) meets F1 . (n + 1) ) )
by A1, A3, A5, Th41;
A7:
dom F = dom F1
by A6, RFINSEQ:3;
then consider P being Permutation of (dom F) such that
A8:
F = F1 * P
by A6, CLASSES1:80;
union (rng F) <> {}
by A1;
then A9:
dom F <> {}
by RELAT_1:42, ZFMISC_1:2;
A10:
dom F = dom G
by A2, FINSEQ_3:29;
then A11:
( dom P = dom G & rng P = dom G )
by A9, FUNCT_2:def 1, FUNCT_2:def 3;
( dom (P ") = rng P & rng (P ") = dom P )
by FUNCT_1:33;
then A12:
dom (G * (P ")) = dom G
by A11, RELAT_1:27;
then A13:
G,G * (P ") are_fiberwise_equipotent
by A10, CLASSES1:80;
reconsider G1 = G * (P ") as FinSequence of ExtREAL by A10, FINSEQ_2:47;
then A16:
Sum G1 = Sum G
by A10, EXTREAL1:11;
A17:
for n being Nat st n in dom F1 holds
G1 . n = diameter (F1 . n)
proof
let n be
Nat;
( n in dom F1 implies G1 . n = diameter (F1 . n) )
assume A18:
n in dom F1
;
G1 . n = diameter (F1 . n)
then A19:
G1 . n = G . ((P ") . n)
by A7, A10, A12, FUNCT_1:12;
reconsider m =
(P ") . n as
Nat ;
A20:
(
m in dom P &
n = P . m )
by A7, A10, A11, A18, FUNCT_1:32;
then
F1 . n = F . m
by A8, FUNCT_1:12;
hence
G1 . n = diameter (F1 . n)
by A4, A19, A20;
verum
end;
defpred S1[ Nat] means ( $1 in dom F1 implies diameter (union (rng (F1 | $1))) <= Sum (G1 | $1) );
A21:
( F1 <> {} & G1 <> {} )
by A2, A7, A9, A12, FINSEQ_3:29;
A23:
S1[ 0 ]
by FINSEQ_3:24;
A24:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A25:
S1[
k]
;
S1[k + 1]
assume A26:
k + 1
in dom F1
;
diameter (union (rng (F1 | (k + 1)))) <= Sum (G1 | (k + 1))
then A27:
( 1
<= k + 1 &
k + 1
<= len F1 )
by FINSEQ_3:25;
per cases
( k = 0 or k <> 0 )
;
suppose
k <> 0
;
diameter (union (rng (F1 | (k + 1)))) <= Sum (G1 | (k + 1))then A31:
1
<= k
by NAT_1:14;
A32:
k < len F1
by A27, NAT_1:13;
then A33:
(diameter (union (rng (F1 | k)))) + (diameter (F1 . (k + 1))) <= (Sum (G1 | k)) + (diameter (F1 . (k + 1)))
by A25, A31, FINSEQ_3:25, XXREAL_3:35;
{(G1 . (k + 1))} c= rng G1
by A7, A10, A12, A26, FUNCT_1:3, ZFMISC_1:31;
then A34:
rng <*(G1 . (k + 1))*> c= rng G1
by FINSEQ_1:38;
A35:
rng G = rng G1
by A13, CLASSES1:75;
then
rng (G1 | k) c= rng G
by FINSEQ_5:19;
then A36:
( not
-infty in rng (G1 | k) & not
-infty in rng <*(G1 . (k + 1))*> )
by A14, A34, A35;
len F1 = len G1
by A7, A10, A12, FINSEQ_3:29;
then
G1 | (k + 1) = (G1 | k) ^ <*(G1 . (k + 1))*>
by A27, NAT_1:13, FINSEQ_5:83;
then Sum (G1 | (k + 1)) =
(Sum (G1 | k)) + (Sum <*(G1 . (k + 1))*>)
by A36, EXTREAL1:10
.=
(Sum (G1 | k)) + (G1 . (k + 1))
by EXTREAL1:8
;
then A37:
(Sum (G1 | k)) + (diameter (F1 . (k + 1))) = Sum (G1 | (k + 1))
by A17, A26;
A38:
F1 . (k + 1) is
open_interval Subset of
REAL
by A22, A26;
A39:
union (rng (F1 | k)) is
open_interval Subset of
REAL
by A6, A22, Th40;
then A40:
(union (rng (F1 | k))) \/ (F1 . (k + 1)) is
interval
by A6, A31, A32, A38, XXREAL_2:89;
F1 | (k + 1) = (F1 | k) ^ <*(F1 . (k + 1))*>
by A27, NAT_1:13, FINSEQ_5:83;
then rng (F1 | (k + 1)) =
(rng (F1 | k)) \/ (rng <*(F1 . (k + 1))*>)
by FINSEQ_1:31
.=
(rng (F1 | k)) \/ {(F1 . (k + 1))}
by FINSEQ_1:38
;
then
union (rng (F1 | (k + 1))) = (union (rng (F1 | k))) \/ (union {(F1 . (k + 1))})
by ZFMISC_1:78;
then
diameter (union (rng (F1 | (k + 1)))) <= (diameter (union (rng (F1 | k)))) + (diameter (F1 . (k + 1)))
by A38, A39, A40, Lm12;
hence
diameter (union (rng (F1 | (k + 1)))) <= Sum (G1 | (k + 1))
by A33, A37, XXREAL_0:2;
verum end;
end;
A41:
for k being Nat holds S1[k]
from NAT_1:sch 2(A23, A24);
A42:
len F1 = len G1
by A7, A10, A12, FINSEQ_3:29;
1 <= len F1
by A21, FINSEQ_1:20;
then
diameter (union (rng (F1 | (len F1)))) <= Sum (G1 | (len F1))
by A41, FINSEQ_3:25;
then
diameter (union (rng F1)) <= Sum (G1 | (len G1))
by A42, FINSEQ_1:58;
then A43:
diameter (union (rng F1)) <= Sum G1
by FINSEQ_1:58;
union (rng (F1 | (len F1))) is open_interval Subset of REAL
by A6, A22, Th40;
then A44:
union (rng F1) is open_interval Subset of REAL
by FINSEQ_1:58;
union (rng F1) = union (rng F)
by A6, CLASSES1:75;
then
diameter A <= diameter (union (rng F1))
by A1, A44, MEASURE5:12;
hence
diameter A <= Sum G
by A16, A43, XXREAL_0:2; verum