Mathlib v3 is deprecated. Go to Mathlib v4

Theorem absorbs_empty

Modification history

2022-04-09 22:07
src/analysis/locally_convex/basic.lean
feat(analysis/locally_convex): every totally bounded set is von Neumann bounded (#13204) …
Modified absorbs_emptyView on Github →
2022-03-14 07:05
src/analysis/locally_convex/basic.lean
chore(analysis/locally_convex/basic): generalize lemmas and add simple lemmas (#12643) …
Added absorbs_emptyView on Github →