The Lebesgue Monotone Convergence Theorem. - Noboru Endou; Keiko Narita; Yasunari Shidama (Formaliz. Math., 2008)

Fatou's Lemma and the Lebesgue's Convergence Theorem. - Noboru Endou; Keiko Narita; Yasunari Shidama (Formaliz. Math., 2008)

Egoroff's Theorem. - Noboru Endou; Yasunari Shidama; Keiko Narita (Formaliz. Math., 2008)

The First Mean Value Theorem for Integrals. - Keiko Narita; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2008)

Integral of Complex-Valued Measurable Function. - Keiko Narita; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2008)

The Measurability of Complex-Valued Functional Sequences. - Keiko Narita; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2009)

Lebesgue's Convergence Theorem of Complex-Valued Function. - Keiko Narita; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2009)

More on the Continuity of Real Functions. - Keiko Narita; Artur Kornilowicz; Yasunari Shidama (Formaliz. Math., 2011)

Differentiable Functions into Real Normed Spaces. - Hiroyuki Okazaki; Noboru Endou; Keiko Narita; Yasunari Shidama (Formaliz. Math., 2011)

The Differentiable Functions from R into Rn. - Keiko Narita; Artur Kornilowicz; Yasunari Shidama (Formaliz. Math., 2012)

Riemann Integral of Functions from ℝ into Real Banach Space. - Keiko Narita; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2013)

The Linearity of Riemann Integral on Functions from ℝ into Real Banach Space. - Keiko Narita; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2013)

Differential Equations on Functions from R into Real Banach Space. - Keiko Narita; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2013)

Dual Spaces and Hahn-Banach Theorem. - Keiko Narita; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2014)

Bidual Spaces and Reflexivity of Real Normed Spaces. - Keiko Narita; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2014)

The Orthogonal Projection and the Riesz Representation Theorem. - Keiko Narita; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2015)

Weak Convergence and Weak Convergence. - Keiko Narita; Yasunari Shidama; Noboru Endou (Formaliz. Math., 2015)

Compactness in Metric Spaces. - Kazuhisa Nakasho; Keiko Narita; Yasunari Shidama (Formaliz. Math., 2016)

The Basic Existence Theorem of Riemann-Stieltjes Integral. - Kazuhisa Nakasho; Keiko Narita; Yasunari Shidama (Formaliz. Math., 2016)

Riemann-Stieltjes Integral. - Keiko Narita; Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2016)

F. Riesz Theorem. - Keiko Narita; Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2017)