:: The One-Dimensional Lebesgue Measure As an Example of a Formalization in the Mizar Language of the Classical Definition of a Mathematical Object
:: by J\'ozef Bia{\l}as
::
:: Received February 4, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

theorem Th1: :: MEASURE7:1
for F being Function of NAT,ExtREAL st ( for n being Element of NAT holds F . n = 0. ) holds
SUM F = 0.
proofend;

theorem Th2: :: MEASURE7:2
for F being Function of NAT,ExtREAL st F is V93() holds
for n being Element of NAT holds F . n <= (Ser F) . n
proofend;

theorem Th3: :: MEASURE7:3
for F, G, H being Function of NAT,ExtREAL st G is V93() &amp; H is V93() &amp; ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) holds
for n being Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n)
proofend;

theorem Th4: :: MEASURE7:4
for F, G, H being Function of NAT,ExtREAL st ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) &amp; G is V93() &amp; H is V93() holds
SUM F <= (SUM G) + (SUM H)
proofend;

theorem Th5: :: MEASURE7:5
for F, G being Function of NAT,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
proofend;

theorem Th6: :: MEASURE7:6
for F being Function of NAT,ExtREAL st F is V93() holds
for n being Element of NAT holds (Ser F) . n <= SUM F
proofend;

definition
let S be non empty set ;
let H be Function of S,ExtREAL;
func On H ->  Function of NAT,ExtREAL means :Def1: :: MEASURE7:def 1
 for n being Element of NAT holds
( ( n in S implies it . n = H . n ) &amp; ( not n in S implies it . n = 0. ) );
existence
 ex b1 being Function of NAT,ExtREAL st
for n being Element of NAT holds
( ( n in S implies b1 . n = H . n ) &amp; ( not n in S implies b1 . n = 0. ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds
( ( n in S implies b1 . n = H . n ) &amp; ( not n in S implies b1 . n = 0. ) ) ) &amp; ( for n being Element of NAT holds
( ( n in S implies b2 . n = H . n ) &amp; ( not n in S implies b2 . n = 0. ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines On MEASURE7:def_1_:_
 for S being non empty set
for H being Function of S,ExtREAL
for b3 being Function of NAT,ExtREAL holds
( b3 = On H iff for n being Element of NAT holds
( ( n in S implies b3 . n = H . n ) &amp; ( not n in S implies b3 . n = 0. ) ) );

theorem Th7: :: MEASURE7:7
for X being non empty set
for G being Function of X,ExtREAL st G is V93() holds
On G is V93()
proofend;

theorem Th8: :: MEASURE7:8
for F being Function of NAT,ExtREAL st F is V93() holds
for n, k being Element of NAT st n <= k holds
(Ser F) . n <= (Ser F) . k
proofend;

theorem Th9: :: MEASURE7:9
for k being Element of NAT
for F being Function of NAT,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. ) &amp; ( for n being Element of NAT st k <= n holds
(Ser F) . n = F . k ) )
proofend;

theorem Th10: :: MEASURE7:10
for G being Function of NAT,ExtREAL st G is V93() 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
proofend;

theorem Th11: :: MEASURE7:11
for F, G being Function of NAT,ExtREAL st G is V93() holds
for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one &amp; ( for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) &amp; ( not k in S implies F . k = 0. ) ) ) holds
SUM F <= SUM G
proofend;

 REAL in bool REAL
by ZFMISC_1:def_1;

then reconsider G0 = NAT --> REAL as Function of NAT,(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
proofend;

definition
let A be Subset of REAL;
mode Interval_Covering of A ->  Function of NAT,(bool REAL) means :Def2: :: MEASURE7:def 2
( A c= union (rng it) &amp; ( for n being Element of NAT holds it . n is Interval ) );
existence
 ex b1 being Function of NAT,(bool REAL) st
( A c= union (rng b1) &amp; ( for n being Element of NAT holds b1 . n is Interval ) ) by Lm2, Lm3, XBOOLE_1:1;
end;

:: deftheorem Def2 defines Interval_Covering MEASURE7:def_2_:_
 for A being Subset of REAL
for b2 being Function of NAT,(bool REAL) holds
( b2 is Interval_Covering of A iff ( A c= union (rng b2) &amp; ( for n being Element of NAT holds b2 . n is Interval ) ) );

definition
let A be Subset of REAL;
let F be Interval_Covering of A;
let n be Element of NAT ;
:: original:.
redefine funcF . n ->  Interval;
correctness
coherence
F . n is Interval;
by Def2;
end;

definition
let F be Function of NAT,(bool REAL);
mode Interval_Covering of F ->  Function of NAT,(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
 ex b1 being Function of NAT,(Funcs (NAT,(bool REAL))) st
for n being Element of NAT holds b1 . n is Interval_Covering of F . n
proofend;
end;

:: deftheorem Def3 defines Interval_Covering MEASURE7:def_3_:_
 for F being Function of NAT,(bool REAL)
for b2 being Function of NAT,(Funcs (NAT,(bool REAL))) holds
( b2 is Interval_Covering of F iff for n being Element of NAT holds b2 . n is Interval_Covering of F . n );

definition
let A be Subset of REAL;
let F be Interval_Covering of A;
deffunc H1( Element of NAT ) ->  Element of ExtREAL = diameter (F . $1);
funcF vol  ->  Function of NAT,ExtREAL means :Def4: :: MEASURE7:def 4
 for n being Element of NAT holds it . n = diameter (F . n);
existence
 ex b1 being Function of NAT,ExtREAL st
for n being Element of NAT holds b1 . n = diameter (F . n)
proofend;
uniqueness
 for b1, b2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds b1 . n = diameter (F . n) ) &amp; ( for n being Element of NAT holds b2 . n = diameter (F . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines vol MEASURE7:def_4_:_
 for A being Subset of REAL
for F being Interval_Covering of A
for b3 being Function of NAT,ExtREAL holds
( b3 = F vol iff for n being Element of NAT holds b3 . n = diameter (F . n) );

theorem Th12: :: MEASURE7:12
for A being Subset of REAL
for F being Interval_Covering of A holds F vol is V93()
proofend;

definition
let F be Function of NAT,(bool REAL);
let H be Interval_Covering of F;
let n be Element of NAT ;
:: original:.
redefine funcH . n ->  Interval_Covering of F . n;
correctness
coherence
H . n is Interval_Covering of F . n;
by Def3;
end;

definition
let F be Function of NAT,(bool REAL);
let G be Interval_Covering of F;
funcG vol  ->  Function of NAT,(Funcs (NAT,ExtREAL)) means :: MEASURE7:def 5
 for n being Element of NAT holds it . n = (G . n) vol ;
existence
 ex b1 being Function of NAT,(Funcs (NAT,ExtREAL)) st
for n being Element of NAT holds b1 . n = (G . n) vol
proofend;
uniqueness
 for b1, b2 being Function of NAT,(Funcs (NAT,ExtREAL)) st ( for n being Element of NAT holds b1 . n = (G . n) vol ) &amp; ( for n being Element of NAT holds b2 . n = (G . n) vol ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines vol MEASURE7:def_5_:_
 for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F
for b3 being Function of NAT,(Funcs (NAT,ExtREAL)) holds
( b3 = G vol iff for n being Element of NAT holds b3 . n = (G . n) vol );

definition
let A be Subset of REAL;
let F be Interval_Covering of A;
func vol F ->  R_eal equals :: MEASURE7:def 6
 SUM (F vol);
correctness
coherence
SUM (F vol) is R_eal;
;
end;

:: 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);

definition
let F be Function of NAT,(bool REAL);
let G be Interval_Covering of F;
func vol G ->  Function of NAT,ExtREAL means :Def7: :: MEASURE7:def 7
 for n being Element of NAT holds it . n = vol (G . n);
existence
 ex b1 being Function of NAT,ExtREAL st
for n being Element of NAT holds b1 . n = vol (G . n)
proofend;
uniqueness
 for b1, b2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds b1 . n = vol (G . n) ) &amp; ( for n being Element of NAT holds b2 . n = vol (G . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines vol MEASURE7:def_7_:_
 for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F
for b3 being Function of NAT,ExtREAL holds
( b3 = vol G iff for n being Element of NAT holds b3 . n = vol (G . n) );

theorem Th13: :: MEASURE7:13
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F
for n being Element of NAT holds 0. <= (vol G) . n
proofend;

definition
let A be Subset of REAL;
defpred S1[ set ] means  ex F being Interval_Covering of A st $1 = vol F;
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
 ex b1 being Subset of ExtREAL st
for x being R_eal holds
( x in b1 iff ex F being Interval_Covering of A st x = vol F )
proofend;
uniqueness
 for b1, b2 being Subset of ExtREAL st ( for x being R_eal holds
( x in b1 iff ex F being Interval_Covering of A st x = vol F ) ) &amp; ( for x being R_eal holds
( x in b2 iff ex F being Interval_Covering of A st x = vol F ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines Svc MEASURE7:def_8_:_
 for A being Subset of REAL
for b2 being Subset of ExtREAL holds
( b2 = Svc A iff for x being R_eal holds
( x in b2 iff ex F being Interval_Covering of A st x = vol F ) );

registration
let A be Subset of REAL;
cluster Svc A ->  non empty ;
coherence
 not Svc A is empty
proofend;
end;

definition
let A be Subset of REAL;
func COMPLEX A ->  Element of ExtREAL  equals :: MEASURE7:def 9
 inf (Svc A);
correctness
coherence
inf (Svc A) is Element of ExtREAL ;
;
end;

:: deftheorem  defines COMPLEX MEASURE7:def_9_:_
 for A being Subset of REAL holds COMPLEX A = inf (Svc A);

definition
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
 ex b1 being Function of (bool REAL),ExtREAL st
for A being Subset of REAL holds b1 . A = inf (Svc A)
proofend;
uniqueness
 for b1, b2 being Function of (bool REAL),ExtREAL st ( for A being Subset of REAL holds b1 . A = inf (Svc A) ) &amp; ( for A being Subset of REAL holds b2 . A = inf (Svc A) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines OS_Meas MEASURE7:def_10_:_
 for b1 being Function of (bool REAL),ExtREAL holds
( b1 = OS_Meas iff for A being Subset of REAL holds b1 . A = inf (Svc A) );

definition
let F be Function of NAT,(bool REAL);
let G be Interval_Covering of F;
let H be Function of NAT,[:NAT,NAT:];
assume B1: 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
 ex b1 being Interval_Covering of union (rng F) st
for n being Element of NAT holds b1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n)
proofend;
uniqueness
 for b1, b2 being Interval_Covering of union (rng F) st ( for n being Element of NAT holds b1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) &amp; ( for n being Element of NAT holds b2 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines On MEASURE7:def_11_:_
 for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F
for H being Function of NAT,[:NAT,NAT:] st rng H = [:NAT,NAT:] holds
for b4 being Interval_Covering of union (rng F) holds
( b4 = On (G,H) iff for n being Element of NAT holds b4 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) );

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

theorem Th14: :: MEASURE7:14
for H being Function of NAT,[:NAT,NAT:] st H is one-to-one &amp; rng H = [:NAT,NAT:] holds
for k being Element of NAT ex m being Element of NAT st
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m
proofend;

theorem Th15: :: MEASURE7:15
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G)
proofend;

theorem Th16: :: MEASURE7:16
OS_Meas is C_Measure of REAL
proofend;

definition
:: original:OS_Meas
redefine func OS_Meas  ->  C_Measure of REAL ;
correctness
coherence
OS_Meas is C_Measure of REAL ;
by Th16;
end;

definition
func Lmi_sigmaFIELD  ->  SigmaField of REAL equals :: MEASURE7:def 12
 sigma_Field OS_Meas;
coherence
 sigma_Field OS_Meas is SigmaField of REAL ;
end;

:: deftheorem  defines Lmi_sigmaFIELD MEASURE7:def_12_:_
 Lmi_sigmaFIELD = sigma_Field OS_Meas;

definition
func L_mi  ->  sigma_Measure of Lmi_sigmaFIELD equals :: MEASURE7:def 13
 sigma_Meas OS_Meas;
correctness
coherence
sigma_Meas OS_Meas is sigma_Measure of Lmi_sigmaFIELD;
;
end;

:: deftheorem  defines L_mi MEASURE7:def_13_:_
 L_mi = sigma_Meas OS_Meas;