convexHull_union_neg_eq_absConvexHull

English

For any subset s, the convex hull of s ∪ (−s) equals the absConvexHull of s.

Русский

Для любого s выполняется: выпуклая оболочка (s ∪ −s) равна absConvexHull(s).

LaTeX

$$$\\operatorname{convexHull}_{\\mathbb{R}}(s \\cup (-s)) = \\operatorname{absConvexHull}_{\\mathbb{R}}(s)$$$

Lean4

@[simp]
theorem convexHull_union_neg_eq_absConvexHull {s : Set E} : convexHull ℝ (s ∪ -s) = absConvexHull ℝ s :=
  by
  rw [absConvexHull_eq_convexHull_balancedHull]
  exact
    le_antisymm
      (convexHull_mono
        (union_subset (subset_balancedHull ℝ) (fun _ _ => by rw [mem_balancedHull_iff]; use -1; simp_all)))
      (by
        rw [← Convex.convexHull_eq (convex_convexHull ℝ (s ∪ -s))]
        exact convexHull_mono balancedHull_subset_convexHull_union_neg)

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