References
- Charalambos D. Aliprantis and Kim C. Border. Infinite dimensional analysis. Springer-Verlag, Berlin, Heidelberg, 2006.
- Vladimir Igorevich Bogachev and Maria Aparecida Soares Ruas. Measure theory, volume 1. Springer, 2007.
- Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving real analysis in Coq: A user-friendly approach to integrals and derivatives. In Chris Hawblitzel and Dale Miller, editors, Certified Programs and Proofs – Second International Conference, CPP 2012, Kyoto, Japan, December 13–15, 2012. Proceedings, volume 7679 of Lecture Notes in Computer Science, pages 289–304. Springer, 2012. doi:10.1007/978-3-642-35308-6 22.
- Noboru Endou. Reconstruction of the one-dimensional Lebesgue measure. Formalized Mathematics, 28(1):93–104, 2020. doi:10.2478/forma-2020-0008.
- Noboru Endou and Yasunari Shidama. Multidimensional measure space and integration. Formalized Mathematics, 31(1):181–192, 2023. doi:10.2478/forma-2023-0017.
- Noboru Endou and Yasunari Shidama. Universality of measure space. Formalized Mathematics, 32(1):149–163, 2024. doi:10.2478/forma-2024-0012.
- Noboru Endou and Yasunari Shidama. Integral of continuous functions of two variables. Formalized Mathematics, 31(1):309–324, 2023. doi:10.2478/forma-2023-0025.
- Noboru Endou and Yasunari Shidama. Integral of continuous three variable functions. Formalized Mathematics, 32(1):9–31, 2024. doi:10.2478/forma-2024-0002.
- Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.
- Johannes Hölzl and Armin Heller. Three chapters of measure theory in Isabelle/HOL. In Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving (ITP 2011), volume 6898 of LNCS, pages 135–151, 2011.
- Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269–275, 2004.
- M.M. Rao. Measure Theory and Integration. Marcel Dekker, 2nd edition, 2004.
- Colin Rothgang, Artur Korniłowicz, and Florian Rabe. A new export of the Mizar Mathematical Library. In Fairouz Kamareddine and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics, pages 205–210, Cham, 2021. Springer International Publishing. doi:10.1007/978-3-030-81097-9 17.
- Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.