Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

## The Measurability of Extended Real Valued Functions

Noboru Endou
Shinshu University, Nagano
Katsumi Wasaki
Shinshu University, Nagano
Yasunari Shidama
Shinshu University, Nagano

### Summary.

In this article we prove the measurablility of some extended real valued functions which are $f$+$g$, $f$\,-\,$g$ and so on. Moreover, we will define the simple function which are defined on the sigma field. It will play an important role for the Lebesgue integral theory.

#### MML Identifier: MESFUNC2

The terminology and notation used in this paper have been introduced in the following articles [20] [22] [1] [21] [17] [23] [11] [2] [18] [3] [4] [5] [10] [19] [6] [7] [8] [9] [12] [13] [14] [15] [16]

#### Contents (PDF format)

1. Finite Valued Function
2. Measurability of $f+g$ and $f - g$
3. Definitions of Extended Real Valued Functions max$_{+}$($f$) and max$_{-}$($f$) and their Basic Properties
4. Measurability of max$_{+}$($f$), max$_{-}$($f$) and $|f|$
5. Definition and Measurability of Characteristic Function
6. Definition and Measurability of Simple Function

#### Bibliography

[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. Zermelo theorem and axiom of choice. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[4] Jozef Bialas. Infimum and supremum of the set of real numbers. Measure theory. Journal of Formalized Mathematics, 2, 1990.
[5] Jozef Bialas. Series of positive real numbers. Measure theory. Journal of Formalized Mathematics, 2, 1990.
[6] Jozef Bialas. The $\sigma$-additive measure theory. Journal of Formalized Mathematics, 2, 1990.
[7] Jozef Bialas. Several properties of the $\sigma$-additive measure. Journal of Formalized Mathematics, 3, 1991.
[8] Jozef Bialas. Completeness of the $\sigma$-additive measure. Measure theory. Journal of Formalized Mathematics, 4, 1992.
[9] Jozef Bialas. Some properties of the intervals. Journal of Formalized Mathematics, 6, 1994.
[10] Czeslaw Bylinski. Basic functions and operations on functions. Journal of Formalized Mathematics, 1, 1989.
[11] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[12] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[13] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[14] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Basic properties of extended real numbers. Journal of Formalized Mathematics, 12, 2000.
[15] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Definitions and basic properties of measurable functions. Journal of Formalized Mathematics, 12, 2000.
[16] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Some properties of extended real numbers operations: abs, min and max. Journal of Formalized Mathematics, 12, 2000.
[17] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.
[18] Andrzej Kondracki. Basic properties of rational numbers. Journal of Formalized Mathematics, 2, 1990.
[19] Andrzej Nedzusiak. Probability. Journal of Formalized Mathematics, 2, 1990.
[20] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[21] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[22] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[23] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.