Theorem WeakDual.metrizable_of_isCompact

Modification history

2025-11-26 07:51
Mathlib/Analysis/Normed/Module/WeakDual.lean
feat(Analysis): the Sequential Banach-Alaoglu theorem (#31656) …
Added WeakDual.metrizable_of_isCompactView on Github →