reconsider y = D as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8;
let H be sequence of [:NAT,NAT:]; ( H is one-to-one & rng H = [:NAT,NAT:] implies for k being Nat ex m being Element of NAT st
for F being sequence of (bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m )
assume that
A1:
H is one-to-one
and
A2:
rng H = [:NAT,NAT:]
; for k being Nat ex m being Element of NAT st
for F being sequence of (bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m
defpred S1[ Nat] means ex m being Element of NAT st
for F being sequence of (bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . $1 <= (Ser (vol G)) . m;
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
set N0 =
{ s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } ;
A4:
{ s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } c= NAT
k + 1
in { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s }
;
then reconsider N0 =
{ s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } as non
empty Subset of
NAT by A4;
given m0 being
Element of
NAT such that A5:
for
F being
sequence of
(bool REAL) for
G being
Interval_Covering of
F holds
(Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m0
;
S1[k + 1]
take m =
m0 + ((pr1 H) . (k + 1));
for F being sequence of (bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m
let F be
sequence of
(bool REAL);
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . mlet G be
Interval_Covering of
F;
(Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m
defpred S2[
Element of
NAT ,
Function]
means ( ( $1
<> (pr1 H) . (k + 1) implies for
m being
Element of
NAT holds $2
. m = (G . $1) . m ) & ( $1
= (pr1 H) . (k + 1) implies for
m being
Element of
NAT holds $2
. m = {} ) );
A6:
for
n being
Element of
NAT ex
y being
Element of
Funcs (
NAT,
(bool REAL)) st
S2[
n,
y]
consider G1 being
sequence of
(Funcs (NAT,(bool REAL))) such that A9:
for
n being
Element of
NAT holds
S2[
n,
G1 . n]
from FUNCT_2:sch 3(A6);
A10:
for
n being
Element of
NAT holds
G1 . n is
Interval_Covering of
D . n
defpred S3[
Element of
N0,
Element of
NAT ]
means $2
= (pr2 H) . $1;
defpred S4[
Element of
NAT ,
Function]
means ( ( $1
= (pr1 H) . (k + 1) implies for
m being
Element of
NAT holds $2
. m = (G . $1) . m ) & ( $1
<> (pr1 H) . (k + 1) implies for
m being
Element of
NAT holds $2
. m = {} ) );
A14:
for
n being
Element of
NAT ex
y being
Element of
Funcs (
NAT,
(bool REAL)) st
S4[
n,
y]
consider G0 being
sequence of
(Funcs (NAT,(bool REAL))) such that A17:
for
n being
Element of
NAT holds
S4[
n,
G0 . n]
from FUNCT_2:sch 3(A14);
for
n being
Element of
NAT holds
G0 . n is
Interval_Covering of
D . n
then reconsider G0 =
G0 as
Interval_Covering of
D by Def3;
set GG0 =
On (
G0,
H);
reconsider G1 =
G1 as
Interval_Covering of
D by A10, Def3;
set GG1 =
On (
G1,
H);
A21:
(Ser ((On (G0,H)) vol)) . (k + 1) <= SUM ((On (G0,H)) vol)
by Th6, Th12;
(On (G1,H)) . (k + 1) =
(G1 . ((pr1 H) . (k + 1))) . ((pr2 H) . (k + 1))
by A2, Def11
.=
{}
by A9
;
then A22:
((On (G1,H)) vol) . (k + 1) = 0.
by Def4, MEASURE5:10;
(Ser ((On (G1,H)) vol)) . (k + 1) = ((Ser ((On (G1,H)) vol)) . k) + (((On (G1,H)) vol) . (k + 1))
by SUPINF_2:def 11;
then A23:
(Ser ((On (G1,H)) vol)) . (k + 1) = (Ser ((On (G1,H)) vol)) . k
by A22, XXREAL_3:4;
for
s being
Element of
NAT holds
0. <= (vol G1) . s
by Th13;
then
vol G1 is
V99()
by SUPINF_2:39;
then A24:
(Ser (vol G1)) . m0 <= (Ser (vol G1)) . m
by SUPINF_2:41;
A25:
for
n being
Element of
NAT holds
((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
proof
let n be
Element of
NAT ;
((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
A26:
(
((On (G0,H)) vol) . n = diameter ((On (G0,H)) . n) &
((On (G1,H)) vol) . n = diameter ((On (G1,H)) . n) )
by Def4;
((On (G,H)) vol) . n = diameter ((On (G,H)) . n)
by Def4;
then A27:
((On (G,H)) vol) . n = diameter ((G . ((pr1 H) . n)) . ((pr2 H) . n))
by A2, Def11;
per cases
( (pr1 H) . n = (pr1 H) . (k + 1) or (pr1 H) . n <> (pr1 H) . (k + 1) )
;
suppose A28:
(pr1 H) . n = (pr1 H) . (k + 1)
;
((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)A29:
(On (G1,H)) . n =
(G1 . ((pr1 H) . n)) . ((pr2 H) . n)
by A2, Def11
.=
{}
by A9, A28
;
(On (G0,H)) . n =
(G0 . ((pr1 H) . n)) . ((pr2 H) . n)
by A2, Def11
.=
(G . ((pr1 H) . n)) . ((pr2 H) . n)
by A17, A28
;
hence
((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
by A26, A27, A29, MEASURE5:10, XXREAL_3:4;
verum end; suppose A30:
(pr1 H) . n <> (pr1 H) . (k + 1)
;
((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)A31:
(On (G0,H)) . n =
(G0 . ((pr1 H) . n)) . ((pr2 H) . n)
by A2, Def11
.=
{}
by A17, A30
;
(On (G1,H)) . n =
(G1 . ((pr1 H) . n)) . ((pr2 H) . n)
by A2, Def11
.=
(G . ((pr1 H) . n)) . ((pr2 H) . n)
by A9, A30
;
hence
((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
by A26, A27, A31, MEASURE5:10, XXREAL_3:4;
verum end; end;
end;
(
(On (G0,H)) vol is
V99() &
(On (G1,H)) vol is
V99() )
by Th12;
then A32:
(Ser ((On (G,H)) vol)) . (k + 1) = ((Ser ((On (G0,H)) vol)) . (k + 1)) + ((Ser ((On (G1,H)) vol)) . (k + 1))
by A25, Th3;
for
s being
Element of
NAT holds
0. <= (vol G1) . s
by Th13;
then A33:
vol G1 is
V99()
by SUPINF_2:39;
(Ser ((On (G1,H)) vol)) . k <= (Ser (vol G1)) . m0
by A5;
then A34:
(Ser ((On (G1,H)) vol)) . (k + 1) <= (Ser (vol G1)) . m
by A23, A24, XXREAL_0:2;
A35:
for
s being
Element of
N0 ex
y being
Element of
NAT st
S3[
s,
y]
;
consider SOS being
Function of
N0,
NAT such that A36:
for
s being
Element of
N0 holds
S3[
s,
SOS . s]
from FUNCT_2:sch 3(A35);
A37:
for
n being
Element of
NAT holds
(vol G) . n = ((vol G0) . n) + ((vol G1) . n)
for
s being
Element of
NAT holds
0. <= (vol G0) . s
by Th13;
then
vol G0 is
V99()
by SUPINF_2:39;
then A46:
(
(vol G0) . ((pr1 H) . (k + 1)) <= (Ser (vol G0)) . ((pr1 H) . (k + 1)) &
(Ser (vol G0)) . ((pr1 H) . (k + 1)) <= (Ser (vol G0)) . m )
by Th2, SUPINF_2:41;
A47:
for
s being
Element of
NAT holds
( (
s in N0 implies
((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ) & ( not
s in N0 implies
((On (G0,H)) vol) . s = 0. ) )
proof
let s be
Element of
NAT ;
( ( s in N0 implies ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ) & ( not s in N0 implies ((On (G0,H)) vol) . s = 0. ) )
thus
(
s in N0 implies
((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s )
( not s in N0 implies ((On (G0,H)) vol) . s = 0. )
assume
not
s in N0
;
((On (G0,H)) vol) . s = 0.
then A51:
not
(pr1 H) . (k + 1) = (pr1 H) . s
;
((On (G0,H)) vol) . s =
diameter ((On (G0,H)) . s)
by Def4
.=
diameter ((G0 . ((pr1 H) . s)) . ((pr2 H) . s))
by A2, Def11
.=
0.
by A17, A51, MEASURE5:10
;
hence
((On (G0,H)) vol) . s = 0.
;
verum
end;
for
s1,
s2 being
object st
s1 in N0 &
s2 in N0 &
SOS . s1 = SOS . s2 holds
s1 = s2
then A56:
SOS is
one-to-one
by FUNCT_2:19;
(G0 . ((pr1 H) . (k + 1))) vol is
V99()
by Th12;
then
SUM ((On (G0,H)) vol) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol)
by A56, A47, Th11;
then A57:
(Ser ((On (G0,H)) vol)) . (k + 1) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol)
by A21, XXREAL_0:2;
SUM ((G0 . ((pr1 H) . (k + 1))) vol) =
vol (G0 . ((pr1 H) . (k + 1)))
.=
(vol G0) . ((pr1 H) . (k + 1))
by Def7
;
then
SUM ((G0 . ((pr1 H) . (k + 1))) vol) <= (Ser (vol G0)) . m
by A46, XXREAL_0:2;
then A58:
(Ser ((On (G0,H)) vol)) . (k + 1) <= (Ser (vol G0)) . m
by A57, XXREAL_0:2;
for
s being
Element of
NAT holds
0. <= (vol G0) . s
by Th13;
then
vol G0 is
V99()
by SUPINF_2:39;
then
(Ser (vol G)) . m = ((Ser (vol G0)) . m) + ((Ser (vol G1)) . m)
by A37, A33, Th3;
hence
(Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m
by A58, A34, A32, XXREAL_3:36;
verum
end;
A59:
S1[ 0 ]
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A59, A3); verum