convexHull_add — Mathlib

English

For sets s and t, the convex hull of their Minkowski sum equals the Minkowski sum of their convex hulls.

Русский

Для множеств s и t выпуклая оболочка их суммы по Минковскому равна сумме выпуклых оболочек s и t.

LaTeX

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

Lean4

theorem convexHull_add (s t : Set E) : convexHull R (s + t) = convexHull R s + convexHull R t := by
  simp_rw [← add_image_prod, ← IsLinearMap.isLinearMap_add.image_convexHull, convexHull_prod]

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