PR #16681: feat(analysis/locally_convex/barrel): barreled...

Stream: triage

[Random Issue Bot]

Today I chose PR 16681 for discussion!

feat(analysis/locally_convex/barrel): barreled spaces
Created by @Anatole Dedecker (@ADedecker) on 2022-09-28
Labels: WIP, modifies-synchronized-file, too-late

Is this PR still relevant? Any recent updates? Anyone making progress?

[Anatole Dedecker]

Well we have docs#BarrelledSpace now, but I'll leave the PR open for now. The reason is that I took a different (and more general) approach to barrelled spaces and Banach-Steinhaus in Lean4, by relying entirely on seminorms instead of docs#LocallyConvexSpace, thus allowing any docs#NontriviallyNormedField. But there are still some geometric characterizations in the case of real vector spaces, and !3#16681 contains some steps towards these.