Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-15 12:30 440e6b3b

View on Github →

feat(topology/algebra/module/locally_convex): define locally convex spaces (#11859)

Estimated changes

Modified src/analysis/seminorm.lean

added theorem normed_space.to_locally_convex_space'

added theorem seminorm.with_seminorms.to_locally_convex_space

Created src/topology/algebra/module/locally_convex.lean

added theorem locally_convex_space.convex_basis_zero

added theorem locally_convex_space.of_bases

added theorem locally_convex_space.of_basis_zero

added theorem locally_convex_space_iff

added theorem locally_convex_space_iff_exists_convex_subset

added theorem locally_convex_space_iff_exists_convex_subset_zero

added theorem locally_convex_space_iff_zero