Riemann Integral of Functions from ℝ into Real Banach Space
Keiko Narita, Noboru Endou, Yasunari Shidama (2013)
Formalized Mathematics
Similarity:
In this article we deal with the Riemann integral of functions from R into a real Banach space. The last theorem establishes the integrability of continuous functions on the closed interval of reals. To prove the integrability we defined uniform continuity for functions from R into a real normed space, and proved related theorems. We also stated some properties of finite sequences of elements of a real normed space and finite sequences of real numbers. In addition we proved some theorems...