mathlib
mathlib copied to clipboard
Banach-Alaoglu for topological vector spaces
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.