Formalization of Separable Version of Banach–Alaoglu Theorem

Okazaki, Hiroyuki; Mieno, Takehiko

doi:10.2478/forma-2025-0018

Abstract

In this article, we first formalize the weak sequential compactness in dual normed spaces; then we prove the separable version of Banach– Alaoglu theorem.

References

Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: a survey of proof assistants and libraries. Mathematical Structures in Computer Science, pages 1–38, 2014.
Search in Google Scholar Back to article
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formal proof of the Lax-Milgram theorem. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 79–89, New York, NY, USA, 2017. Association for Computing Machinery. doi:10.1145/3018610.3018625.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
Johannes Hölzl, Fabian Immler, and Brian Hu man. Type classes and filters for mathematical analysis in Isabelle/HOL. In Interactive Theorem Proving, pages 279–294. Springer, 2013.
Search in Google Scholar Back to article
Isao Miyadera. Functional Analysis. Riko-Gaku-Sya, 1972.
Search in Google Scholar Back to article
Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Implicit function theorem. Part I. Formalized Mathematics, 25(4):269–281, 2017. doi:10.1515/forma-2017-0026.
Search in Google Scholar Back to article
Lawrence Narici and Edward Beckenstein. Topological Vector Spaces. Chapman and Hall/CRC, 2010. doi:10.1201/9781584888673.
Search in Google Scholar Back to article
Keiko Narita, Noboru Endou, and Yasunari Shidama. Weak convergence and weak* convergence. Formalized Mathematics, 23(3):231–241, 2015. doi:10.1515/forma-2015-0019.
Search in Google Scholar Back to article
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-917.
Search in Google Scholar Back to article
Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.
Search in Google Scholar Back to article
Laurent Schwartz. Cours d’analyse. Hermann, 1981.
Search in Google Scholar Back to article
Kôsaku Yosida. Functional Analysis. Springer, 1980.
Search in Google Scholar Back to article

Formalization of Separable Version of Banach–Alaoglu Theorem

Abstract

Paradigm

My account