Locally convex spaces and convinient vector spaces

Stream: Is there code for X?

[Tomas Skrivan]

Looking at the mathlib documentation, there is not a library for locally convex spaces. Is someone working on it?

Also, I would be really interested in having formalization of convinient vector spaces. I'm interested in doing differentiable programming and since convinient vector spaces form a closed cartesion category they should be the ideal setting for formalizing this.

[Yury G. Kudryashov]

There is a PR #1926 with local convexity but it seems that the author is not interested in getting it merged.

[Yury G. Kudryashov]

I think that you may take over this PR if you want.

[Tomas Skrivan]

Nice, I will look into it but I'm not sure if I have the time to take over this.