convex_sum — Mathlib

English

If each t(i) is convex for i in a finite set s, then the sum over i ∈ s of t(i) is convex.

Русский

Если для каждого i из конечного множества s множество t(i) выпукло, то сумма по i∈s выпукла.

LaTeX

$$$\forall i \in s, Convex 𝕜 (t i) \to Convex 𝕜 (\sum i \in s, t i)$$$

Lean4

theorem convex_sum {ι} {s : Finset ι} (t : ι → Set E) (h : ∀ i ∈ s, Convex 𝕜 (t i)) : Convex 𝕜 (∑ i ∈ s, t i) :=
  (convexAddSubmonoid 𝕜 E).sum_mem h

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