The One-Dimensional Lebesgue Measure

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)