Mathlib v3 is deprecated. Go to Mathlib v4

Theorem seminorm.with_seminorms.to_locally_convex_space

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.to_locally_convex_spaceView on Github →
2022-02-15 12:30
src/analysis/seminorm.lean
feat(topology/algebra/module/locally_convex): define locally convex spaces (#11859)
Added seminorm.with_seminorms.to_locally_convex_spaceView on Github →