convexBodySum_convex — Mathlib

English

For any fixed B, the set convexBodySum K B is a convex subset of the mixed space.

Русский

Для фиксированного B множество convexBodySum K B выпукло в смешанном пространстве.

LaTeX

$$Convex(\\mathbb{R}) (convexBodySum K B)$$

Lean4

theorem convexBodySum_convex : Convex ℝ (convexBodySum K B) :=
  by
  refine Convex_subadditive_le (fun _ _ => convexBodySumFun_add_le _ _) (fun c x h => ?_) B
  convert le_of_eq (convexBodySumFun_smul c x)
  exact (abs_eq_self.mpr h).symm

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