This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Banach-Alaoglu for topological vector spaces #15734
Labels
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
We should have almost everything to prove the general Banach-Alaoglu theorem. One reference would be Chapter 8 in the book by Narici-Beckenstein. The main ingredients still missing are the completeness of the algebraic dual (Thm 8.2.9) and the equivalence of weakly bounded and weakly totally bounded (Thm 8.2.8). The proof of the Banach-Alaoglu theorem for Banach spaces might be helpful as well.
The text was updated successfully, but these errors were encountered: