convexBodySum_isBounded — Mathlib

English

The family convexBodySum K B is bounded (in the product topology).

Русский

Семейство convexBodySum K B ограничено (в произведённой топологии).

LaTeX

$$Bornology.IsBounded (convexBodySum K B)$$

Lean4

theorem convexBodySum_isBounded : Bornology.IsBounded (convexBodySum K B) := by
  classical
  refine Metric.isBounded_iff.mpr ⟨B + B, fun x hx y hy => ?_⟩
  refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)
  · exact le_trans (norm_le_convexBodySumFun x) hx
  · exact le_trans (norm_le_convexBodySumFun y) hy

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