Absolutely convex hull of a totally bounded set

Stream: maths

[Christopher Hoskin]

Hello,

I've been doing some work on absolutely convex hulls #17029, #17204.

The first PR #17029 is straight-forward - it sets up the absolutely convex hull as a closure operator and establishes basic properties closely following what's currently in Mathlib for the convex hull.

In the second PR #17204 I establish that the absolutely convex hull of a totally bounded set is totally bounded, following the proof given in Bourbaki TVS II.25. However, the PR is rather long and ugly due to the translation between the uniformity and neighbourhoods of a point. Before I put any effort into golfing the current proof, I thought it was worth asking if I am barking up the wrong tree and there is some other approach I should be taking to the proof? (I have a passing awareness of uniformities and filters, but I don't have much experience working with them.)

Thanks,

Christopher

[Patrick Massot]

@Anatole Dedecker this sounds like something you may like to investigate.

[Anatole Dedecker]

Indeed, let me have a look at this.