On L1 Space Formed by Real-Valued Partial Functions
Watase, Yasushige, Endou, Noboru, Shidama, Yasunari
Formalization of Integral Linear Space
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Partial Differentiation on Normed Linear Spaces Rn
Endou, Noboru, Shidama, Yasunari, Miyajima, Keiichi
Conservation Rules of Direct Sum Decomposition of Groups
Nakasho, Kazuhisa, Yamazaki, Hiroshi, Okazaki, Hiroyuki, Shidama, Yasunari
Differentiation of Vector-Valued Functions on n-Dimensional Real Normed Linear Spaces
Inoué, Takao, Endou, Noboru, Shidama, Yasunari
Isomorphisms of Direct Products of Finite Cyclic Groups
Arai, Kenichi, Okazaki, Hiroyuki, Shidama, Yasunari
Fatou's Lemma and the Lebesgue's Convergence Theorem
Endou, Noboru, Narita, Keiko, Shidama, Yasunari
The Product Space of Real Normed Spaces and its Properties
Endou, Noboru, Shidama, Yasunari, Miyajima, Keiichi
Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers
Yamazaki, Hiroshi, Endou, Noboru, Shidama, Yasunari, Okazaki, Hiroyuki
Cartesian Products of Family of Real Linear Spaces
Okazaki, Hiroyuki, Endou, Noboru, Shidama, Yasunari
Riemann Integral of Functions from R into Rn
Miyajima, Keiichi, Shidama, Yasunari
Extended Euclidean Algorithm and CRT Algorithm
Okazaki, Hiroyuki, Aoki, Yosiki, Shidama, Yasunari