Mathlib v3 is deprecated. Go to Mathlib v4

Theorem seminorm.with_seminorms_of_has_basis

Modification history

2022-03-19 19:33
src/analysis/seminorm.lean
refactor(analysis/seminorm): move topology induced by seminorms to its own file (#12826) …
Deleted seminorm.with_seminorms_of_has_basisView on Github →
2022-03-14 07:05
src/analysis/seminorm.lean
feat(analysis/seminorm): add lemmas for `with_seminorms` (#12649) …
Added seminorm.with_seminorms_of_has_basisView on Github →