Theorem WeakDual.exists_countable_separating

Modification history

2026-04-03 20:10
Mathlib/Analysis/Normed/Module/WeakDual.lean
chore(Analysis/Normed/Module/WeakDual): revert `polar`, `polar_def` and `isClosed_polar` to weaker hypotheses (#37314) …
Modified WeakDual.exists_countable_separatingView on Github →
2025-11-26 07:51
Mathlib/Analysis/Normed/Module/WeakDual.lean
feat(Analysis): the Sequential Banach-Alaoglu theorem (#31656) …
Added WeakDual.exists_countable_separatingView on Github →