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] [IsUniformAddGroup E] [LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E] (hs : TotallyBounded s) : TotallyBounded ((convexHull ℝ) s)

@[simp]

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