Theorem WeakDual.withSeminorms

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.withSeminorms View on Github →