mathlib3

feat(analysis/locally_convex/barrel): barreled spaces

#16681

Open