Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-09 22:07 4c4e5e83

View on Github →

feat(analysis/locally_convex): every totally bounded set is von Neumann bounded (#13204) Add one lemma and some cleanups of previous PR.

Estimated changes

modified theorem absorbs.add
modified theorem absorbs_empty