F. Riesz Theorem

SummaryIn this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first section, we defined Mizar functor ClstoCmp, compact topological spaces as closed interval subset of real numbers. Then using the former definition and referring to the article [10] and the article [5], we defined the normed spaces of continuous functions on closed interval subset of real numbers, and defined the normed spaces of bounded functions on closed interval subset of real numbers. We also proved some related properties.In Sec.2, we proved some lemmas for the proof of F. Riesz theorem. In Sec.3, we proved F. Riesz theorem, about the dual space of the space of continuous functions on closed interval subset of real numbers, finally. We applied Hahn-Banach theorem (36) in [7], to the proof of the last theorem. For the description of theorems of this section, we also referred to the article [8] and the article [6]. These formalizations are based on [2], [3], [9], and [11].Narita Keiko - Hirosaki-city, Aomori, JapanNakasho Kazuhisa - Akita Prefectural University, Akita, JapanShidama Yasunari - Shinshu University, Nagano, JapanGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Haim Brezis. Functional Analysis, Sobolev Spaces and Partial Differential Equations. Springer, 2011.Peter D. Dax. Functional Analysis. Pure and Applied Mathematics: A Wiley Series of Texts, Monographs and Tracts. Wiley Interscience, 2002.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.Katuhiko Kanazashi, Noboru Endou, and Yasunari Shidama. Banach algebra of continuous functionals and the space of real-valued continuous functionals with bounded support. Formalized Mathematics, 18(1):11–16, 2010. doi:10.2478/v10037-010-0002-1.Kazuhisa Nakasho, Keiko Narita, and Yasunari Shidama. The basic existence theorem of Riemann-Stieltjes integral. Formalized Mathematics, 24(4):253–259, 2016. doi:10.1515/forma-2016-0021.Keiko Narita, Noboru Endou, and Yasunari Shidama. Dual spaces and Hahn-Banach theorem. Formalized Mathematics, 22(1):69–77, 2014. doi:10.2478/forma-2014-0007.Keiko Narita, Kazuhisa Nakasho, and Yasunari Shidama. Riemann-Stieltjes integral. Formalized Mathematics, 24(3):199–204, 2016. doi:10.1515/forma-2016-0016.Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.Yasunari Shidama, Hikofumi Suzuki, and Noboru Endou. Banach algebra of bounded functionals. Formalized Mathematics, 16(2):115–122, 2008. doi:10.2478/v10037-008-0017-z.Kosaku Yoshida. Functional Analysis. Springer, 1980.25317918