Theorem exists_nhds_hasAntitoneBasis_absConvex_open_add_closure_subset

Modification history

2026-06-10 13:05
Mathlib/Analysis/LocallyConvex/AbsConvex.lean
feat(Topology/Algebra/Module/LocallyConvex): a very nice basis of locally convex spaces (#39063) …
Added exists_nhds_hasAntitoneBasis_absConvex_open_add_closure_subsetView on Github →