<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In the Mizar system ([1], [2]), Józef Białas has already given the one-dimensional Lebesgue measure [4]. However, the measure introduced by Biał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 and also it cannot 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 [7], [3].</p></abstract>

In the Mizar system ([1], [2]), Józef Białas has already given the one-dimensional Lebesgue measure [4]. However, the measure introduced by Biał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 and also it cannot 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 [7], [3].

Reconstruction of the One-Dimensional Lebesgue Measure

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 License.

{"article-title":"Reconstruction of the One-Dimensional Lebesgue Measure"}

In the Mizar system ([1], [2]), Józef Białas has already given the one-dimensional Lebesgue measure [4]. However, the measure introduced by Białas limited the...

Reconstruction of the One-Dimensional Lebesgue Measure

Published Online: May 29, 2020

Page range: 93 - 104

Accepted: Jan 13, 2020

DOI: https://doi.org/10.2478/forma-2020-0008

Keywords
Lebesgue measure, algebra of intervals

© 2020 Noboru Endou, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 License.

Reconstruction of the One-Dimensional Lebesgue Measure

Published Online: May 29, 2020

Page range: 93 - 104

Accepted: Jan 13, 2020

DOI: https://doi.org/10.2478/forma-2020-0008

KeywordsLebesgue measure, algebra of intervals

© 2020 Noboru Endou, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 License.

Keywords
Lebesgue measure, algebra of intervals