Mathlib v3 is deprecated. Go to Mathlib v4

Theorem locally_convex_space_iff_exists_convex_subset

Modification history

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_iff_exists_convex_subset View on Github →