Lebesgue's Convergence Theorem of Complex-Valued Function
Keiko Narita, Noboru Endou, Yasunari Shidama (2009)
Formalized Mathematics
Similarity:
In this article, we formalized Lebesgue's Convergence theorem of complex-valued function. We proved Lebesgue's Convergence Theorem of realvalued function using the theorem of extensional real-valued function. Then applying the former theorem to real part and imaginary part of complex-valued functional sequences, we proved Lebesgue's Convergence Theorem of complex-valued function. We also defined partial sums of real-valued functional sequences and complex-valued functional sequences...