convexHullAddMonoidHom — Mathlib

English

The convex hull operation is additive with respect to pointwise addition of sets; i.e., convexHull respects Minkowski addition of sets.

Русский

Операция выпуклой оболочки сохраняет сложение множеств по точечному прибавлению; выпуклая оболочка совместима с суммой Минковского.

LaTeX

$$$\operatorname{conv}(R, s \,+\, t) = \operatorname{conv}(R, s) \,+\, \operatorname{conv}(R, t)$$$

Lean4

/-- `convexHull` is an additive monoid morphism under pointwise addition. -/
@[simps]
noncomputable def convexHullAddMonoidHom : Set E →+ Set E
    where
  toFun := convexHull R
  map_add' := convexHull_add
  map_zero' := convexHull_zero

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