Mathlib v3 is deprecated. Go to Mathlib v4

Theorem locally_convex_space.convex_open_basis_zero

Modification history

2022-10-23 16:03

src/topology/algebra/module/locally_convex.lean

feat(topology/algebra/module/locally_convex): generalize `disjoint.exists_open_convexes` to locally convex spaces (#16749)

Added locally_convex_space.convex_open_basis_zero View on Github →