Formalization of Separable Version of Banach–Alaoglu Theorem (Formalized Mathematics, 2025)