Theorem nhds_basis_abs_convex

Modification history

2024-10-17 07:12
Mathlib/Analysis/LocallyConvex/AbsConvex.lean
feat(Analysis/LocallyConvex/AbsConvex): Define the Absolutely Convex Hull (#17029) …
Deleted nhds_basis_abs_convexView on Github →
2023-05-25 08:46
Mathlib/Analysis/LocallyConvex/AbsConvex.lean
feat: port Analysis.LocallyConvex.AbsConvex (#4320)
Added nhds_basis_abs_convexView on Github →