Mathlib v3 is deprecated. Go to Mathlib v4

Theorem locally_convex_space_induced

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) …

Added locally_convex_space_induced View on Github →