totallyBounded_absConvexHull — Mathlib

English

If a subset s is totally bounded, then its absConvexHull is totally bounded.

Русский

Если s полностью ограничено, то absConvexHull(s) полностью ограничено.

LaTeX

$$$TotallyBounded\\bigl(\\operatorname{absConvexHull}_{\\mathbb{R}}(s)\\bigr)$$$

Lean4

theorem totallyBounded_absConvexHull (hs : TotallyBounded s) : TotallyBounded (absConvexHull ℝ s) :=
  by
  rw [← convexHull_union_neg_eq_absConvexHull]
  apply totallyBounded_convexHull
  rw [totallyBounded_union]
  exact ⟨hs, totallyBounded_neg hs⟩

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