convex_multiset_sum — Mathlib

English

The sum of a multiset of convex sets is convex if each element is convex.

Русский

Сумма мультисета выпуклых множеств выпукла, если каждое множество выпукло.

LaTeX

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

Lean4

theorem convex_multiset_sum {s : Multiset (Set E)} (h : ∀ i ∈ s, Convex 𝕜 i) : Convex 𝕜 s.sum :=
  (convexAddSubmonoid 𝕜 E).multiset_sum_mem _ h

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