:: 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
::
:: Copyright (c) 1995-2021 Association of Mizar Users

theorem Th1: :: MEASURE7:1
for F being sequence of ExtREAL st ( for n being Element of NAT holds F . n = 0. ) holds
SUM F = 0.
proof end;

theorem Th2: :: MEASURE7:2
for F being sequence of ExtREAL st F is V99() holds
for n being Nat holds F . n <= (Ser F) . n
proof end;

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)
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)
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
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
proof end;

definition
let S be non empty set ;
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
ex b1 being sequence of ExtREAL st
for n being Element of NAT holds
( ( n in S implies b1 . n = H . n ) & ( not n in S implies b1 . n = 0. ) )
proof end;
uniqueness
for b1, b2 being sequence of ExtREAL st ( for n being Element of NAT holds
( ( n in S implies b1 . n = H . n ) & ( not n in S implies b1 . n = 0. ) ) ) & ( for n being Element of NAT holds
( ( n in S implies b2 . n = H . n ) & ( not n in S implies b2 . n = 0. ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines On MEASURE7:def 1 :
for S being non empty set
for H being Function of S,ExtREAL
for b3 being sequence of ExtREAL holds
( b3 = On H iff for n being Element of NAT holds
( ( n in S implies b3 . n = H . n ) & ( 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 V99() holds
On G is V99()
proof end;

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
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 ) )
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
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
proof end;

by ZFMISC_1:def 1;

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

Lm1:
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;
mode Interval_Covering of A -> sequence of () means :Def2: :: MEASURE7:def 2
( A c= union (rng it) & ( for n being Element of NAT holds it . n is Interval ) );
existence
ex b1 being sequence of () st
( A c= union (rng b1) & ( for n being Element of NAT holds b1 . n is Interval ) )
by ;
end;

:: deftheorem Def2 defines Interval_Covering MEASURE7:def 2 :
for A being Subset of REAL
for b2 being sequence of () holds
( b2 is Interval_Covering of A iff ( A c= union (rng b2) & ( 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 func F . n -> Interval;
correctness
coherence
F . n is Interval
;
by Def2;
end;

definition
let F be sequence of ();
mode Interval_Covering of F -> sequence of (Funcs (NAT,())) means :Def3: :: MEASURE7:def 3
for n being Element of NAT holds it . n is Interval_Covering of F . n;
existence
ex b1 being sequence of (Funcs (NAT,())) st
for n being Element of NAT holds b1 . n is Interval_Covering of F . n
proof end;
end;

:: deftheorem Def3 defines Interval_Covering MEASURE7:def 3 :
for F being sequence of ()
for b2 being sequence of (Funcs (NAT,())) 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); func F vol -> sequence of ExtREAL means :Def4: :: MEASURE7:def 4 for n being Element of NAT holds it . n = diameter (F . n); existence ex b1 being sequence of ExtREAL st for n being Element of NAT holds b1 . n = diameter (F . n) proof end; uniqueness for b1, b2 being sequence of ExtREAL st ( for n being Element of NAT holds b1 . n = diameter (F . n) ) & ( for n being Element of NAT holds b2 . n = diameter (F . n) ) holds b1 = b2 proof end; end; :: deftheorem Def4 defines vol MEASURE7:def 4 : for A being Subset of REAL for F being Interval_Covering of A for b3 being sequence of 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 V99() proof end; definition let F be sequence of (); 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; definition let F be sequence of (); let G be Interval_Covering of F; func G vol -> sequence of () means :: MEASURE7:def 5 for n being Element of NAT holds it . n = (G . n) vol ; existence ex b1 being sequence of () st for n being Element of NAT holds b1 . n = (G . n) vol proof end; uniqueness for b1, b2 being sequence of () st ( for n being Element of NAT holds b1 . n = (G . n) vol ) & ( for n being Element of NAT holds b2 . n = (G . n) vol ) holds b1 = b2 proof end; end; :: deftheorem defines vol MEASURE7:def 5 : for F being sequence of () for G being Interval_Covering of F for b3 being sequence of () 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 sequence of (); 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 ex b1 being sequence of ExtREAL st for n being Element of NAT holds b1 . n = vol (G . n) proof end; uniqueness for b1, b2 being sequence of ExtREAL st ( for n being Element of NAT holds b1 . n = vol (G . n) ) & ( for n being Element of NAT holds b2 . n = vol (G . n) ) holds b1 = b2 proof end; end; :: deftheorem Def7 defines vol MEASURE7:def 7 : for F being sequence of () for G being Interval_Covering of F for b3 being sequence of 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 sequence of () 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 S1[ object ] 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 )
proof end;
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 ) ) & ( for x being R_eal holds
( x in b2 iff ex F being Interval_Covering of A st x = vol F ) ) holds
b1 = b2
proof end;
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
proof end;
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 (),ExtREAL means :Def10: :: MEASURE7:def 10
for A being Subset of REAL holds it . A = inf (Svc A);
existence
ex b1 being Function of (),ExtREAL st
for A being Subset of REAL holds b1 . A = inf (Svc A)
proof end;
uniqueness
for b1, b2 being Function of (),ExtREAL st ( for A being Subset of REAL holds b1 . A = inf (Svc A) ) & ( for A being Subset of REAL holds b2 . A = inf (Svc A) ) holds
b1 = b2
proof end;
end;

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

definition
let F be sequence of ();
let G be Interval_Covering of F;
let H be sequence of ;
assume A1: rng H = ;
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)
proof end;
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) ) & ( for n being Element of NAT holds b2 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines On MEASURE7:def 11 :
for F being sequence of ()
for G being Interval_Covering of F
for H being sequence of st rng H = 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 --> () as sequence of () ;

theorem Th14: :: MEASURE7:14
for H being sequence of st H is one-to-one & rng H = holds
for k being Nat ex m being Element of NAT st
for F being sequence of ()
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 ()
for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G)
proof end;

theorem Th16: :: MEASURE7:16
proof end;

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

definition
coherence ;
end;

:: deftheorem defines Lmi_sigmaFIELD MEASURE7:def 12 :

definition
correctness ;
end;

:: deftheorem defines L_mi MEASURE7:def 13 :