Mathlib v3 is deprecated. Go to Mathlib v4

Theorem locally_convex_space.of_bases

Modification history

2022-06-11 11:06
src/topology/algebra/module/locally_convex.lean
feat(topology/algebra/module/locally_convex): local convexity is preserved by `Inf` and `induced` (#12118) …
Modified locally_convex_space.of_basesView on Github →
2022-02-15 12:30
src/topology/algebra/module/locally_convex.lean
feat(topology/algebra/module/locally_convex): define locally convex spaces (#11859)
Added locally_convex_space.of_basesView on Github →