Theorem WeakDual.isSeqCompact_of_isBounded_of_isClosed

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.isSeqCompact_of_isBounded_of_isClosedView on Github →
2025-11-26 07:51
Mathlib/Analysis/Normed/Module/WeakDual.lean
feat(Analysis): the Sequential Banach-Alaoglu theorem (#31656) …
Added WeakDual.isSeqCompact_of_isBounded_of_isClosedView on Github →