convexHull_sum — Mathlib

English

The convex hull of the sum of a multiset of sets equals the sum of their convex hulls, via a map under a convexHull additive monoid hom.

Русский

Выпуклая оболочка суммы мультимножества множеств равна сумме их выпуклых оболочек через отображение выпуклой оболочки как моноида.

LaTeX

$$$\operatorname{conv}(R, s.sum) = \operatorname{map}(\operatorname{conv}(R), s).sum$$$

Lean4

theorem convexHull_sum {ι} (s : Finset ι) (t : ι → Set E) : convexHull R (∑ i ∈ s, t i) = ∑ i ∈ s, convexHull R (t i) :=
  map_sum (convexHullAddMonoidHom R E) _ _

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