Commit 2022-05-04 20:04 91c0ef86

feat(analysis/normed_space/weak_dual): add the rest of Banach-Alaoglu theorem (#9862) The second of two parts to add the Banach-Alaoglu theorem about the compactness of the closed unit ball (and more generally polar sets of neighborhoods of the origin) of the dual of a normed space in the weak-star topology. This second half is about the embedding of the weak dual of a normed space into a (big) product of the ground fields, and the required compactness statements from Tychonoff's theorem. In particular it contains the actual Banach-Alaoglu theorem. Co-Authored-By: Yury Kudryashov urkud@urkud.name