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][bourbaki1987]
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)