convexHull_prod — Mathlib

English

The convex hull of the sum of a list of sets equals the sum (Minkowski sum) of their convex hulls.

Русский

Выпуклая оболочка суммы списка множеств равна сумме (Минковского суммы) их выпуклых оболочек.

LaTeX

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

Lean4

@[simp]
theorem convexHull_prod (s : Set E) (t : Set F) : convexHull R (s ×ˢ t) = convexHull R s ×ˢ convexHull R t :=
  Subset.antisymm
      (convexHull_min (prod_mono (subset_convexHull _ _) <| subset_convexHull _ _) <|
        (convex_convexHull _ _).prod <| convex_convexHull _ _) <|
    prod_subset_iff.2 fun _ hx _ => mk_mem_convexHull_prod hx

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