<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

Publicado en línea: 29 may 2020

Páginas: 93 - 104

Aceptado: 13 ene 2020

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

Palabras clave
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

Publicado en línea: 29 may 2020

Páginas: 93 - 104

Aceptado: 13 ene 2020

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

Palabras claveLebesgue measure, algebra of intervals

© 2020 Noboru Endou, published by Sciendo

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

Palabras clave
Lebesgue measure, algebra of intervals