:: by J\'ozef Bia{\l}as

::

:: Received February 4, 1995

:: Copyright (c) 1995-2021 Association of Mizar Users

theorem Th3: :: MEASURE7:3

for F, G, H being sequence of ExtREAL st G is V99() & H is V99() & ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) holds

for n being Nat holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n)

for n being Nat holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n)

proof end;

theorem Th4: :: MEASURE7:4

for F, G, H being sequence of ExtREAL st ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) & G is V99() & H is V99() holds

SUM F <= (SUM G) + (SUM H)

SUM F <= (SUM G) + (SUM H)

proof end;

theorem Th5: :: MEASURE7:5

for F, G being sequence of ExtREAL st ( for n being Element of NAT holds F . n <= G . n ) holds

for n being Element of NAT holds (Ser F) . n <= SUM G

for n being Element of NAT holds (Ser F) . n <= SUM G

proof end;

theorem Th6: :: MEASURE7:6

for F being sequence of ExtREAL st F is V99() holds

for n being Element of NAT holds (Ser F) . n <= SUM F

for n being Element of NAT holds (Ser F) . n <= SUM F

proof end;

definition

let S be non empty set ;

let H be Function of S,ExtREAL;

ex b_{1} being sequence of ExtREAL st

for n being Element of NAT holds

( ( n in S implies b_{1} . n = H . n ) & ( not n in S implies b_{1} . n = 0. ) )

for b_{1}, b_{2} being sequence of ExtREAL st ( for n being Element of NAT holds

( ( n in S implies b_{1} . n = H . n ) & ( not n in S implies b_{1} . n = 0. ) ) ) & ( for n being Element of NAT holds

( ( n in S implies b_{2} . n = H . n ) & ( not n in S implies b_{2} . n = 0. ) ) ) holds

b_{1} = b_{2}

end;
let H be Function of S,ExtREAL;

func On H -> sequence of ExtREAL means :Def1: :: MEASURE7:def 1

for n being Element of NAT holds

( ( n in S implies it . n = H . n ) & ( not n in S implies it . n = 0. ) );

existence for n being Element of NAT holds

( ( n in S implies it . n = H . n ) & ( not n in S implies it . n = 0. ) );

ex b

for n being Element of NAT holds

( ( n in S implies b

proof end;

uniqueness for b

( ( n in S implies b

( ( n in S implies b

b

proof end;

:: deftheorem Def1 defines On MEASURE7:def 1 :

for S being non empty set

for H being Function of S,ExtREAL

for b_{3} being sequence of ExtREAL holds

( b_{3} = On H iff for n being Element of NAT holds

( ( n in S implies b_{3} . n = H . n ) & ( not n in S implies b_{3} . n = 0. ) ) );

for S being non empty set

for H being Function of S,ExtREAL

for b

( b

( ( n in S implies b

theorem Th8: :: MEASURE7:8

for F being sequence of ExtREAL st F is V99() holds

for n, k being Nat st n <= k holds

(Ser F) . n <= (Ser F) . k

for n, k being Nat st n <= k holds

(Ser F) . n <= (Ser F) . k

proof end;

theorem Th9: :: MEASURE7:9

for k being Nat

for F being sequence of ExtREAL st ( for n being Element of NAT st n <> k holds

F . n = 0. ) holds

( ( for n being Element of NAT st n < k holds

(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds

(Ser F) . n = F . k ) )

for F being sequence of ExtREAL st ( for n being Element of NAT st n <> k holds

F . n = 0. ) holds

( ( for n being Element of NAT st n < k holds

(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds

(Ser F) . n = F . k ) )

proof end;

theorem Th10: :: MEASURE7:10

for G being sequence of ExtREAL st G is V99() holds

for S being non empty Subset of NAT

for H being Function of S,NAT st H is one-to-one holds

SUM (On (G * H)) <= SUM G

for S being non empty Subset of NAT

for H being Function of S,NAT st H is one-to-one holds

SUM (On (G * H)) <= SUM G

proof end;

theorem Th11: :: MEASURE7:11

for F, G being sequence of ExtREAL st G is V99() holds

for S being non empty Subset of NAT

for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds

( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds

SUM F <= SUM G

for S being non empty Subset of NAT

for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds

( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds

SUM F <= SUM G

proof end;

REAL in bool REAL

by ZFMISC_1:def 1;

then reconsider G0 = NAT --> REAL as sequence of (bool REAL) by FUNCOP_1:45;

Lm1: rng G0 = {REAL}

by FUNCOP_1:8;

then Lm2: REAL c= union (rng G0)

by ZFMISC_1:25;

Lm3: for n being Element of NAT holds G0 . n is Interval

proof end;

definition

let A be Subset of REAL;

ex b_{1} being sequence of (bool REAL) st

( A c= union (rng b_{1}) & ( for n being Element of NAT holds b_{1} . n is Interval ) )
by Lm2, Lm3, XBOOLE_1:1;

end;
mode Interval_Covering of A -> sequence of (bool REAL) means :Def2: :: MEASURE7:def 2

( A c= union (rng it) & ( for n being Element of NAT holds it . n is Interval ) );

existence ( A c= union (rng it) & ( for n being Element of NAT holds it . n is Interval ) );

ex b

( A c= union (rng b

:: deftheorem Def2 defines Interval_Covering MEASURE7:def 2 :

for A being Subset of REAL

for b_{2} being sequence of (bool REAL) holds

( b_{2} is Interval_Covering of A iff ( A c= union (rng b_{2}) & ( for n being Element of NAT holds b_{2} . n is Interval ) ) );

for A being Subset of REAL

for b

( b

definition

let A be Subset of REAL;

let F be Interval_Covering of A;

let n be Element of NAT ;

:: original: .

redefine func F . n -> Interval;

correctness

coherence

F . n is Interval;

by Def2;

end;
let F be Interval_Covering of A;

let n be Element of NAT ;

:: original: .

redefine func F . n -> Interval;

correctness

coherence

F . n is Interval;

by Def2;

definition

let F be sequence of (bool REAL);

ex b_{1} being sequence of (Funcs (NAT,(bool REAL))) st

for n being Element of NAT holds b_{1} . n is Interval_Covering of F . n

end;
mode Interval_Covering of F -> sequence of (Funcs (NAT,(bool REAL))) means :Def3: :: MEASURE7:def 3

for n being Element of NAT holds it . n is Interval_Covering of F . n;

existence for n being Element of NAT holds it . n is Interval_Covering of F . n;

ex b

for n being Element of NAT holds b

proof end;

:: deftheorem Def3 defines Interval_Covering MEASURE7:def 3 :

for F being sequence of (bool REAL)

for b_{2} being sequence of (Funcs (NAT,(bool REAL))) holds

( b_{2} is Interval_Covering of F iff for n being Element of NAT holds b_{2} . n is Interval_Covering of F . n );

for F being sequence of (bool REAL)

for b

( b

definition

let A be Subset of REAL;

let F be Interval_Covering of A;

deffunc H_{1}( Element of NAT ) -> Element of ExtREAL = diameter (F . $1);

ex b_{1} being sequence of ExtREAL st

for n being Element of NAT holds b_{1} . n = diameter (F . n)

for b_{1}, b_{2} being sequence of ExtREAL st ( for n being Element of NAT holds b_{1} . n = diameter (F . n) ) & ( for n being Element of NAT holds b_{2} . n = diameter (F . n) ) holds

b_{1} = b_{2}

end;
let F be Interval_Covering of A;

deffunc H

func F vol -> sequence of ExtREAL means :Def4: :: MEASURE7:def 4

for n being Element of NAT holds it . n = diameter (F . n);

existence for n being Element of NAT holds it . n = diameter (F . n);

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines vol MEASURE7:def 4 :

for A being Subset of REAL

for F being Interval_Covering of A

for b_{3} being sequence of ExtREAL holds

( b_{3} = F vol iff for n being Element of NAT holds b_{3} . n = diameter (F . n) );

for A being Subset of REAL

for F being Interval_Covering of A

for b

( b

definition

let F be sequence of (bool REAL);

let H be Interval_Covering of F;

let n be Element of NAT ;

:: original: .

redefine func H . n -> Interval_Covering of F . n;

correctness

coherence

H . n is Interval_Covering of F . n;

by Def3;

end;
let H be Interval_Covering of F;

let n be Element of NAT ;

:: original: .

redefine func H . n -> Interval_Covering of F . n;

correctness

coherence

H . n is Interval_Covering of F . n;

by Def3;

definition

let F be sequence of (bool REAL);

let G be Interval_Covering of F;

ex b_{1} being sequence of (Funcs (NAT,ExtREAL)) st

for n being Element of NAT holds b_{1} . n = (G . n) vol

for b_{1}, b_{2} being sequence of (Funcs (NAT,ExtREAL)) st ( for n being Element of NAT holds b_{1} . n = (G . n) vol ) & ( for n being Element of NAT holds b_{2} . n = (G . n) vol ) holds

b_{1} = b_{2}

end;
let G be Interval_Covering of F;

func G vol -> sequence of (Funcs (NAT,ExtREAL)) means :: MEASURE7:def 5

for n being Element of NAT holds it . n = (G . n) vol ;

existence for n being Element of NAT holds it . n = (G . n) vol ;

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines vol MEASURE7:def 5 :

for F being sequence of (bool REAL)

for G being Interval_Covering of F

for b_{3} being sequence of (Funcs (NAT,ExtREAL)) holds

( b_{3} = G vol iff for n being Element of NAT holds b_{3} . n = (G . n) vol );

for F being sequence of (bool REAL)

for G being Interval_Covering of F

for b

( b

definition

let A be Subset of REAL;

let F be Interval_Covering of A;

correctness

coherence

SUM (F vol) is R_eal;

;

end;
let F be Interval_Covering of A;

correctness

coherence

SUM (F vol) is R_eal;

;

:: deftheorem defines vol MEASURE7:def 6 :

for A being Subset of REAL

for F being Interval_Covering of A holds vol F = SUM (F vol);

for A being Subset of REAL

for F being Interval_Covering of A holds vol F = SUM (F vol);

definition

let F be sequence of (bool REAL);

let G be Interval_Covering of F;

ex b_{1} being sequence of ExtREAL st

for n being Element of NAT holds b_{1} . n = vol (G . n)

for b_{1}, b_{2} being sequence of ExtREAL st ( for n being Element of NAT holds b_{1} . n = vol (G . n) ) & ( for n being Element of NAT holds b_{2} . n = vol (G . n) ) holds

b_{1} = b_{2}

end;
let G be Interval_Covering of F;

func vol G -> sequence of ExtREAL means :Def7: :: MEASURE7:def 7

for n being Element of NAT holds it . n = vol (G . n);

existence for n being Element of NAT holds it . n = vol (G . n);

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines vol MEASURE7:def 7 :

for F being sequence of (bool REAL)

for G being Interval_Covering of F

for b_{3} being sequence of ExtREAL holds

( b_{3} = vol G iff for n being Element of NAT holds b_{3} . n = vol (G . n) );

for F being sequence of (bool REAL)

for G being Interval_Covering of F

for b

( b

theorem Th13: :: MEASURE7:13

for F being sequence of (bool REAL)

for G being Interval_Covering of F

for n being Element of NAT holds 0. <= (vol G) . n

for G being Interval_Covering of F

for n being Element of NAT holds 0. <= (vol G) . n

proof end;

definition

let A be Subset of REAL;

defpred S_{1}[ object ] means ex F being Interval_Covering of A st $1 = vol F;

ex b_{1} being Subset of ExtREAL st

for x being R_eal holds

( x in b_{1} iff ex F being Interval_Covering of A st x = vol F )

for b_{1}, b_{2} being Subset of ExtREAL st ( for x being R_eal holds

( x in b_{1} iff ex F being Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds

( x in b_{2} iff ex F being Interval_Covering of A st x = vol F ) ) holds

b_{1} = b_{2}

end;
defpred S

func Svc A -> Subset of ExtREAL means :Def8: :: MEASURE7:def 8

for x being R_eal holds

( x in it iff ex F being Interval_Covering of A st x = vol F );

existence for x being R_eal holds

( x in it iff ex F being Interval_Covering of A st x = vol F );

ex b

for x being R_eal holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def8 defines Svc MEASURE7:def 8 :

for A being Subset of REAL

for b_{2} being Subset of ExtREAL holds

( b_{2} = Svc A iff for x being R_eal holds

( x in b_{2} iff ex F being Interval_Covering of A st x = vol F ) );

for A being Subset of REAL

for b

( b

( x in b

registration
end;

:: deftheorem defines COMPLEX MEASURE7:def 9 :

for A being Subset of REAL holds COMPLEX A = inf (Svc A);

for A being Subset of REAL holds COMPLEX A = inf (Svc A);

definition

ex b_{1} being Function of (bool REAL),ExtREAL st

for A being Subset of REAL holds b_{1} . A = inf (Svc A)

for b_{1}, b_{2} being Function of (bool REAL),ExtREAL st ( for A being Subset of REAL holds b_{1} . A = inf (Svc A) ) & ( for A being Subset of REAL holds b_{2} . A = inf (Svc A) ) holds

b_{1} = b_{2}
end;

func OS_Meas -> Function of (bool REAL),ExtREAL means :Def10: :: MEASURE7:def 10

for A being Subset of REAL holds it . A = inf (Svc A);

existence for A being Subset of REAL holds it . A = inf (Svc A);

ex b

for A being Subset of REAL holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines OS_Meas MEASURE7:def 10 :

for b_{1} being Function of (bool REAL),ExtREAL holds

( b_{1} = OS_Meas iff for A being Subset of REAL holds b_{1} . A = inf (Svc A) );

for b

( b

definition

let F be sequence of (bool REAL);

let G be Interval_Covering of F;

let H be sequence of [:NAT,NAT:];

assume A1: rng H = [:NAT,NAT:] ;

ex b_{1} being Interval_Covering of union (rng F) st

for n being Element of NAT holds b_{1} . n = (G . ((pr1 H) . n)) . ((pr2 H) . n)

for b_{1}, b_{2} being Interval_Covering of union (rng F) st ( for n being Element of NAT holds b_{1} . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) & ( for n being Element of NAT holds b_{2} . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) holds

b_{1} = b_{2}

end;
let G be Interval_Covering of F;

let H be sequence of [:NAT,NAT:];

assume A1: rng H = [:NAT,NAT:] ;

func On (G,H) -> Interval_Covering of union (rng F) means :Def11: :: MEASURE7:def 11

for n being Element of NAT holds it . n = (G . ((pr1 H) . n)) . ((pr2 H) . n);

existence for n being Element of NAT holds it . n = (G . ((pr1 H) . n)) . ((pr2 H) . n);

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines On MEASURE7:def 11 :

for F being sequence of (bool REAL)

for G being Interval_Covering of F

for H being sequence of [:NAT,NAT:] st rng H = [:NAT,NAT:] holds

for b_{4} being Interval_Covering of union (rng F) holds

( b_{4} = On (G,H) iff for n being Element of NAT holds b_{4} . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) );

for F being sequence of (bool REAL)

for G being Interval_Covering of F

for H being sequence of [:NAT,NAT:] st rng H = [:NAT,NAT:] holds

for b

( b

reconsider D = NAT --> ({} REAL) as sequence of (bool REAL) ;

theorem Th14: :: MEASURE7:14

for H being sequence of [:NAT,NAT:] st H is one-to-one & rng H = [:NAT,NAT:] holds

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

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

proof end;

theorem Th15: :: MEASURE7:15

for F being sequence of (bool REAL)

for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G)

for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G)

proof end;

definition

:: original: OS_Meas

redefine func OS_Meas -> C_Measure of REAL ;

correctness

coherence

OS_Meas is C_Measure of REAL ;

by Th16;

end;
redefine func OS_Meas -> C_Measure of REAL ;

correctness

coherence

OS_Meas is C_Measure of REAL ;

by Th16;