Mathlib v3 is deprecated. Go to Mathlib v4

Theorem normed_space.to_locally_convex_space'

Modification history

2022-03-19 19:33
src/analysis/locally_convex/with_seminorms.lean
refactor(analysis/seminorm): move topology induced by seminorms to its own file (#12826) …
Modified normed_space.to_locally_convex_space'View on Github →
2022-02-15 12:30
src/analysis/seminorm.lean
feat(topology/algebra/module/locally_convex): define locally convex spaces (#11859)
Added normed_space.to_locally_convex_space'View on Github →