convexBodySumFun_add_le — Mathlib

English

convexBodySumFun x = 0 if and only if x = 0.

Русский

convexBodySumFun x = 0 тогда и только тогда, когда x = 0.

LaTeX

$$convexBodySumFun(x) = 0 \\iff x = 0$$

Lean4

theorem convexBodySumFun_add_le (x y : mixedSpace K) :
    convexBodySumFun (x + y) ≤ convexBodySumFun x + convexBodySumFun y :=
  by
  simp_rw [convexBodySumFun, ← Finset.sum_add_distrib, ← mul_add]
  exact Finset.sum_le_sum fun _ _ ↦ mul_le_mul_of_nonneg_left (normAtPlace_add_le _ x y) (Nat.cast_pos.mpr mult_pos).le

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