Formalization of Integral Linear Space
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Riemann Integral of Functions from R into Rn
Miyajima, Keiichi, Shidama, Yasunari
Submodule of free Z-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Differentiability Properties of Lipschitzian Bilinear Operators in Real Normed Spaces
Nakasho, Kazuhisa, Shidama, Yasunari
Dual Spaces and Hahn-Banach Theorem
Narita, Keiko, Endou, Noboru, Shidama, Yasunari
More on Continuous Functions on Normed Linear Spaces
Okazaki, Hiroyuki, Endou, Noboru, Shidama, Yasunari
Convex Sets and Convex Combinations on Complex Linear Spaces
Matsuzaki, Hidenori, Endou, Noboru, Shidama, Yasunari
Continuity of Bounded Linear Operators on Normed Linear Spaces
Nakasho, Kazuhisa, Futa, Yuichi, Shidama, Yasunari
Riemann-Stieltjes Integral
Narita, Keiko, Nakasho, Kazuhisa, Shidama, Yasunari
Isomorphism Theorem on Vector Spaces over a Ring
Futa, Yuichi, Shidama, Yasunari
Integral of Continuous Functions of Two Variables
Endou, Noboru, Shidama, Yasunari
Multidimensional Measure Space and Integration
Endou, Noboru, Shidama, Yasunari