Theorem WeakDual.isBounded_toWeakDual_preimage_iff_isBounded

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_toWeakDual_preimage_iff_isBoundedView on Github →