convexBodySumFun_smul — Mathlib

English

For any real c and x in the mixed space, convexBodySumFun(c · x) = |c| · convexBodySumFun(x).

Русский

Гомогенность: convexBodySumFun(c · x) = |c| · convexBodySumFun(x).

LaTeX

$$\$ convexBodySumFun( c \\cdot x ) = |c| \\cdot convexBodySumFun(x) \$$$

Lean4

theorem convexBodySumFun_smul (c : ℝ) (x : mixedSpace K) : convexBodySumFun (c • x) = |c| * convexBodySumFun x := by
  simp_rw [convexBodySumFun, normAtPlace_smul, ← mul_assoc, mul_comm, Finset.mul_sum, mul_assoc]

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