Formalization of Separable Version of Banach–Alaoglu Theorem

Summary In this article, we first formalize the weak sequential compactness in dual normed spaces; then we prove the separable version of Banach– Alaoglu theorem.