Boundedness and diameter of closed convex hulls

Taking the closed convex hull of a set in a real seminormed space preserves both boundedness and diameter. These are the closed-hull counterparts of isBounded_convexHull and convexHull_diam.

@[simp]

theorem TauCeti.isBounded_closedConvexHull {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} : Bornology.IsBounded ((closedConvexHull ℝ) K) ↔ Bornology.IsBounded K

A closed convex hull is bounded exactly when the original set is.

@[simp]

theorem TauCeti.diam_closedConvexHull {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} : Metric.diam ((closedConvexHull ℝ) K) = Metric.diam K

Taking the closed convex hull preserves the diameter.