:: 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-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, NUMBERS, SUBSET_1, SUPINF_2, ARYTM_3, CARD_1, RELAT_1,
      TARSKI, ORDINAL2, XXREAL_0, NAT_1, XXREAL_2, ORDINAL1, XBOOLE_0,
      ZFMISC_1, FUNCOP_1, MEASURE5, FUNCT_2, SUPINF_1, MCART_1, MEASURE4,
      REAL_1, PROB_1, MEASURE1, MEASURE7, FUNCT_7, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, ORDINAL1,
      NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, XXREAL_3, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NAT_1, PROB_1, XXREAL_2, SUPINF_1,
      SUPINF_2, MEASURE1, MEASURE4, MEASURE5, RECDEF_1;
 constructors PARTFUN1, DOMAIN_1, FUNCOP_1, NAT_1, MEASURE4, MEASURE5,
      RECDEF_1, SUPINF_1, XREAL_0, RELSET_1, XXREAL_2, MEASURE1, PROB_2;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0,
      MEMBERED, MEASURE1, MEASURE4, VALUED_0, XXREAL_2, XXREAL_3, FUNCT_1,
      RELSET_1, XXREAL_0;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Some theorems about series of R_eal numbers

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

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

theorem :: MEASURE7:3
  for F,G,H being sequence of ExtREAL st G is nonnegative & H
  is nonnegative holds (for n being Element of NAT holds F.n = G.n + H.n )
  implies for n being Nat holds (Ser F).n = (Ser G).n + (Ser H).n;

theorem :: MEASURE7:4
  for F,G,H being sequence of ExtREAL st for n being Element of
NAT holds F.n = G.n + H.n holds G is nonnegative & H is nonnegative implies SUM
  (F) <= SUM(G) + SUM(H);

theorem :: MEASURE7:5
  for F,G being sequence of ExtREAL holds ( for n being Element
of NAT holds F.n <= G.n) implies for n being Element of NAT holds (Ser(F)).n <=
  SUM(G);

theorem :: MEASURE7:6
  for F being sequence of ExtREAL holds F is nonnegative
  implies for n being Element of NAT holds (Ser(F)).n <= SUM(F);

definition
  let S be non empty set;
  let H be Function of S,ExtREAL;
  func On H -> sequence of ExtREAL means
:: 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.);
end;

theorem :: MEASURE7:7
  for X being non empty set for G being Function of X,ExtREAL st G
  is nonnegative holds On G is nonnegative;

theorem :: MEASURE7:8
  for F being sequence of ExtREAL st F is nonnegative holds for
  n,k being Nat st n <= k holds Ser(F).n <= Ser(F).k;

theorem :: MEASURE7:9
  for k being Nat holds for F being sequence of
ExtREAL holds ((for n being Element of NAT st n <> k holds F.n = 0.) implies (
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 );

theorem :: MEASURE7:10
  for G being sequence of ExtREAL st G is nonnegative holds
for S being non empty Subset of NAT holds for H being Function of S,NAT st H is
  one-to-one holds SUM(On(G*H)) <= SUM(G);

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

definition
  let A be Subset of REAL;
  mode Interval_Covering of A -> sequence of  bool REAL means
:: MEASURE7:def 2

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

definition
  let A be Subset of REAL;
  let F be Interval_Covering of A;
  let n be Element of NAT;
  redefine func F.n ->Interval;
end;

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

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

definition
  let A be Subset of REAL;
  let F be Interval_Covering of A;
  func F vol -> sequence of ExtREAL means
:: MEASURE7:def 4

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

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

definition
  let F be sequence of  bool REAL;
  let H be Interval_Covering of F;
  let n be Element of NAT;
  redefine func H.n -> Interval_Covering of F.n;
end;

definition
  let F be sequence of  bool REAL;
  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;
end;

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

definition
  let F be sequence of (bool REAL);
  let G be Interval_Covering of F;
  func vol(G) -> sequence of ExtREAL means
:: MEASURE7:def 7

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

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

definition
  let A be Subset of REAL;
  func Svc(A) -> Subset of ExtREAL means
:: MEASURE7:def 8

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

registration
  let A be Subset of REAL;
  cluster Svc(A) -> non empty;
end;

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

definition
  func OS_Meas -> Function of bool REAL,ExtREAL means
:: MEASURE7:def 10

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

definition

  let F be sequence of bool REAL;
  let G be Interval_Covering of F;
  let H be sequence of [:NAT,NAT:] such that
 rng H = [:NAT,NAT:];
  func On(G,H) -> Interval_Covering of union rng F means
:: MEASURE7:def 11

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

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

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

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

definition
  redefine func OS_Meas -> C_Measure of REAL;
end;

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

definition
  func L_mi -> sigma_Measure of Lmi_sigmaFIELD equals
:: MEASURE7:def 13
  sigma_Meas(OS_Meas);
end;