Theorem WeakDual.isBounded_closedBall

Modification history

2026-03-23 18:23

Mathlib/Analysis/Normed/Module/WeakDual.lean

feat(Analysis/Normed/Module/WeakDual): register bornology and boundedness API (#36332) …

Added WeakDual.isBounded_closedBall View on Github →