Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

The One-Dimensional Lebesgue Measure


Jozef Bialas
Lodz University, Lodz

Summary.

The paper is the crowning of a series of articles written in the Mizar language, being a formalization of notions needed for the description of the one-dimensional Lebesgue measure. The formalization of the notion as classical as the Lebesgue measure determines the powers of the PC Mizar system as a tool for the strict, precise notation and verification of the correctness of deductive theories. Following the successive articles [2], [3], [4], [8] constructed so that the final one should include the definition and the basic properties of the Lebesgue measure, we observe one of the paths relatively simple in the sense of the definition, enabling us the formal introduction of this notion. This way, although toilsome, since such is the nature of formal theories, is greatly instructive. It brings home the proper succession of the introduction of the definitions of intermediate notions and points out to those elements of the theory which determine the essence of the complexity of the notion being introduced.\par The paper includes the definition of the $\sigma$-field of Lebesgue measurable sets, the definition of the Lebesgue measure and the basic set of the theorems describing its properties.

MML Identifier: MEASURE7

The terminology and notation used in this paper have been introduced in the following articles [12] [11] [15] [13] [14] [16] [9] [2] [3] [4] [5] [6] [7] [10] [1]

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek and Piotr Rudnicki. On defining functions on trees. Journal of Formalized Mathematics, 5, 1993.
[2] Jozef Bialas. Infimum and supremum of the set of real numbers. Measure theory. Journal of Formalized Mathematics, 2, 1990.
[3] Jozef Bialas. Series of positive real numbers. Measure theory. Journal of Formalized Mathematics, 2, 1990.
[4] Jozef Bialas. The $\sigma$-additive measure theory. Journal of Formalized Mathematics, 2, 1990.
[5] Jozef Bialas. Completeness of the $\sigma$-additive measure. Measure theory. Journal of Formalized Mathematics, 4, 1992.
[6] Jozef Bialas. Properties of Caratheodor's measure. Journal of Formalized Mathematics, 4, 1992.
[7] Jozef Bialas. Properties of the intervals of real numbers. Journal of Formalized Mathematics, 5, 1993.
[8] Jozef Bialas. Some properties of the intervals. Journal of Formalized Mathematics, 6, 1994.
[9] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[10] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[11] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[12] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[13] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[14] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[15] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[16] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received February 4, 1995


[ Download a postscript version, MML identifier index, Mizar home page]