isBounded_convexHull — Mathlib

English

Convex hull is bounded if and only if the original set is bounded.

Русский

Выпуклая оболочка ограничена тогда и только тогда, когда множество ограничено.

LaTeX

$$Bornology.IsBounded (convexHull ℝ s) ↔ Bornology.IsBounded s$$

Lean4

/-- Convex hull of `s` is bounded if and only if `s` is bounded. -/
@[simp]
theorem isBounded_convexHull {s : Set E} : Bornology.IsBounded (convexHull ℝ s) ↔ Bornology.IsBounded s := by
  simp only [Metric.isBounded_iff_ediam_ne_top, convexHull_ediam]

Похожие утверждения