Integral of Complex-Valued Measurable Function
説明
Summary. In this article, we formalized the notion of the integral of a complex-valued function considered as a sum of its real and imaginary parts. Then we defined the measurability and integrability in this context, and proved the linearity and several other basic properties of complex-valued measurable functions. The set of properties showed in this paper is based on [15], where the case of real-valued measurable functions is considered. MML identifier: MESFUN6C, version: 7.9.01 4.101.1015
収録刊行物
-
- Formalized Mathematics
-
Formalized Mathematics 16 2008-01-01
Walter de Gruyter GmbH
