@MISC{MEASUR12.MIZ,
  AUTHOR = {Endou, Noboru},
  TITLE = {Reconstruction of the One-Dimensional Lebesgue Measure},
  DAY = {13},
  MONTH = {January},
  YEAR = {2020},
  ADDRESS1 = {National Institute of Technology, Gifu College\\2236-2 Kamimakuwa, Motosu, Gifu, Japan},
  SECTION1 = {Properties of intervals},
  SECTION2 = {Tools for extended real sequences},
  SECTION3 = {Open Covering of Intervals},
  SECTION4 = {Measure of intervals by OS_Meas},
  SECTION5 = {Construction of the one-dimensional Lebesque measure},
  SUMMARY = {In Mizar System, J\'ozef Bia{\l}as has already given the one-dimensional Lebesgue
  measure \cite{MEASURE7.abs}. However, the measure intrduced by Bia{\l}as limited the outer
  measure to a field with finite additivity. So, although it satisfies the nature of the measure,
  it cannot specify the length of measurable sets. Also it can not determine what kind of set is
  a measurable set.
   From the above, the authors first determined the length of the interval by the outer measure.
  Specifically, we used the compactness of the real space.
  Next, we constructed the pre-measure by limiting the outer measure to a semialgebra of
  intervals. Furthermore, by repeating the extension of the previous measure, we reconstructed
  the one-dimensional Lebesgue measure \cite{FOLLAND},\cite{Bauer:2002}.}}
