Theorem nhds_hasBasis_absConvex_open

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) …
Modified nhds_hasBasis_absConvex_openView on Github →
2025-10-14 23:03
Mathlib/Analysis/LocallyConvex/AbsConvex.lean
refactor(Analysis/LocallyConvex/AbsConvex): Redefine AbsConvex to use a single ring of scalars (#29342) …
Modified nhds_hasBasis_absConvex_openView on Github →
2024-10-17 07:12
Mathlib/Analysis/LocallyConvex/AbsConvex.lean
feat(Analysis/LocallyConvex/AbsConvex): Define the Absolutely Convex Hull (#17029) …
Added nhds_hasBasis_absConvex_openView on Github →