Totally Bounded sets and Convex Hulls

Main statements

• totallyBounded_convexHull The convex hull of a totally bounded set is totally bounded.

References

• Bourbaki, Topological Vector Spaces

Tags

convex, totally bounded

theorem totallyBounded_convexHull (E : Type u_1) {s : Set E} [AddCommGroup E] [Module ℝ E] [UniformSpace E] [UniformAddGroup E] [lcs : LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E] (hs : TotallyBounded s) : TotallyBounded ((convexHull ℝ) s)