Riemann Integral of Functions R into C
Keiichi Miyajima, Takahiro Kato, Yasunari Shidama (2010)
Formalized Mathematics
Similarity:
In this article, we define the Riemann Integral on functions R into C and proof the linearity of this operator. Especially, the Riemann integral of complex functions is constituted by the redefinition about the Riemann sum of complex numbers. Our method refers to the [19].