Formalization of Separable Version of Banach–Alaoglu Theorem

Pole DC	Wartość	Język
dc.contributor.author	Okazaki, Hiroyuki	-
dc.contributor.author	Mieno, Takehiko	-
dc.date.accessioned	2026-02-02T12:56:03Z	-
dc.date.available	2026-02-02T12:56:03Z	-
dc.date.issued	2025	-
dc.identifier.citation	Formalized Mathematics, Volume 33, Issue 1, Pages 231-236	pl
dc.identifier.issn	1426-2630	-
dc.identifier.uri	http://hdl.handle.net/11320/19738	-
dc.description.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.	pl
dc.language.iso	en	pl
dc.publisher	University of Białystok	pl
dc.rights	Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)	pl
dc.rights.uri	https://creativecommons.org/licenses/by-sa/4.0/	pl
dc.subject	dual space	pl
dc.subject	orthonormal complement	pl
dc.subject	minimum norm problem	pl
dc.title	Formalization of Separable Version of Banach–Alaoglu Theorem	pl
dc.type	Article	pl
dc.rights.holder	2025 The Author(s)	pl
dc.rights.holder	CC BY-SA 4.0 license	pl
dc.identifier.doi	10.2478/forma-2025-0018	-
dc.description.Affiliation	Hiroyuki Okazaki - Shinshu University, Nagano, Japan	pl
dc.description.Affiliation	Takehiko Mieno - Shinshu University, Epson Avasys Corporation, Nagano, Japan	pl
dc.description.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.	pl
dc.description.references	Sylvie Boldo, Francois Clement, 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.	pl
dc.description.references	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.	pl
dc.description.references	Johannes Holzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Interactive Theorem Proving, pages 279–294. Springer, 2013.	pl
dc.description.references	Isao Miyadera. Functional Analysis. Riko-Gaku-Sya, 1972.	pl
dc.description.references	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.	pl
dc.description.references	Lawrence Narici and Edward Beckenstein. Topological Vector Spaces. Chapman and Hall/CRC, 2010. doi:10.1201/9781584888673.	pl
dc.description.references	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.	pl
dc.description.references	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.	pl
dc.description.references	Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.	pl
dc.description.references	Laurent Schwartz. Cours d’analyse. Hermann, 1981.	pl
dc.description.references	Kosaku Yosida. Functional Analysis. Springer, 1980.	pl
dc.identifier.eissn	1898-9934	-
dc.description.volume	33	pl
dc.description.issue	1	pl
dc.description.firstpage	231	pl
dc.description.lastpage	236	pl
dc.identifier.citation2	Formalized Mathematics	pl
Występuje w kolekcji(ach):	Formalized Mathematics, 2025, Volume 33, Issue 1

Pliki w tej pozycji:

Plik	Opis	Rozmiar	Format
Formalization_of_Separable_Version_of_Banach–Alaoglu_Theorem.pdf		226,23 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL