<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

Pubblicato online: 29 mag 2020

Pagine: 93 - 104

Accettato: 13 gen 2020

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

Parole chiave
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

Pubblicato online: 29 mag 2020

Pagine: 93 - 104

Accettato: 13 gen 2020

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

Parole chiaveLebesgue measure, algebra of intervals

© 2020 Noboru Endou, published by Sciendo

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

Parole chiave
Lebesgue measure, algebra of intervals