no goals
ι : Type ?u.42300
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
⊢ Metric.Bounded (↑(convexHull ℝ).toOrderHom s) ↔ Metric.Bounded s
simp only [Metric.bounded_iff_ediam_ne_top, convexHull_ediam]