convexHull_list_sum — Mathlib

English

The same additive property of convex hull extends to lists and their images under the convex hull operator, with a simp-friendly presentation.

Русский

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

LaTeX

$$$\operatorname{conv}(R, l.sum) = \bigl(\text{map convexHull } R \bigr)(l).sum$$$

Lean4

theorem convexHull_list_sum (l : List (Set E)) : convexHull R l.sum = (l.map <| convexHull R).sum :=
  map_list_sum (convexHullAddMonoidHom R E) l

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