<abstract xml:lang="en" xmlns="http://www.w3.org/1999/xhtml"><p>In this article, we formalized the measurability of complex-valued functional sequences. First, we proved the measurability of the limits of real-valued functional sequences. Next, we defined complex-valued functional sequences dividing real part into imaginary part. Then using the former theorems, we proved the measurability of each part. Lastly, we proved the measurability of the limits of complex-valued functional sequences. We also showed several properties of complex-valued measurable functions. In addition, we proved properties of complex-valued simple functions.</p></abstract>

In this article, we formalized the measurability of complex-valued functional sequences. First, we proved the measurability of the limits of real-valued functional sequences. Next, we defined complex-valued functional sequences dividing real part into imaginary part. Then using the former theorems, we proved the measurability of each part. Lastly, we proved the measurability of the limits of complex-valued functional sequences. We also showed several properties of complex-valued measurable functions. In addition, we proved properties of complex-valued simple functions.

The Measurability of Complex-Valued Functional Sequences

Gifu National College of Technology, Japan

Formalized Mathematics

{"article-title":"The Measurability of Complex-Valued Functional Sequences"}

In this article, we formalized the measurability of complex-valued functional sequences. First, we proved the measurability of the limits of real-valued...

The Measurability of Complex-Valued Functional Sequences

Published Online: Jul 14, 2009

Page range: 89 - 97

DOI: https://doi.org/10.2478/v10037-009-0010-1

This content is open access.