Formalization of separable version of Banach-Alaoglu theorem

DOI10.2478/FORMA-2025-0018MaRDI QIDQ6840578zbMATH OpenFDO

Authors Hiroyuki Okazaki, Takehiko Mieno

Publication date 23 March 2026

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 4.0 International

Full work available at URL https://doi.org/10.2478/FORMA-2025-0018

zbMATH Keywords

dual spaceminimum norm problemorthonormal complement

Mathematics Subject Classification ID

Compactness in topological linear spaces; angelic spaces, etc. (46A50) Compactness in Banach (or normed) spaces (46B50) Dual spaces of operator algebras (47L50) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A new export of the Mizar mathematical library
• Four decades of \textsc{Mizar}. Foreword
• scientific article; zbMATH DE number 3678487 (Why is no real title available?)
• scientific article; zbMATH DE number 1022519 (Why is no real title available?)
• Implicit function theorem. I
• Topological vector spaces
• Type classes and filters for mathematical analysis in Isabelle/HOL
• Weak convergence and weak\(^\ast\) convergence

This page was built for publication: Formalization of separable version of Banach-Alaoglu theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6840578)