Mathlib v3 is deprecated. Go to Mathlib v4

Theorem totally_bounded.is_vonN_bounded

Modification history

2022-04-09 22:07
src/analysis/locally_convex/bounded.lean
feat(analysis/locally_convex): every totally bounded set is von Neumann bounded (#13204) …
Added totally_bounded.is_vonN_boundedView on Github →