<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

Data publikacji: 29 maj 2020

Zakres stron: 93 - 104

Przyjęty: 13 sty 2020

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

Słowa kluczowe
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

Data publikacji: 29 maj 2020

Zakres stron: 93 - 104

Przyjęty: 13 sty 2020

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

Słowa kluczoweLebesgue measure, algebra of intervals

© 2020 Noboru Endou, published by Sciendo

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

Słowa kluczowe
Lebesgue measure, algebra of intervals