convexHull_multiset_sum — Mathlib

English

For a finite index family, the convex hull of a finite sum is the sum of convex hulls: conv(R, ∑ i t_i) = ∑ i conv(R, t_i).

Русский

Для конечной индексации выпуклая оболочка суммы равна сумме выпуклых оболочек: conv(R, ∑ i t_i) = ∑ i conv(R, t_i).

LaTeX

$$$\operatorname{conv}(R, \sum_i t_i) = \sum_i \operatorname{conv}(R, t_i)$$$

Lean4

theorem convexHull_multiset_sum (s : Multiset (Set E)) : convexHull R s.sum = (s.map <| convexHull R).sum :=
  map_multiset_sum (convexHullAddMonoidHom R E) s

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