absConvexHull_eq_convexHull_balancedHull

English

The absolute convex hull of s equals the convex hull of the balanced hull of s.

Русский

Абсолютно выпуклая оболочка s равна выпуклой оболочке сбалансированного баланса s.

LaTeX

$$$$ \\operatorname{absConvexHull}_{\\mathbb{k}}(s) = \\operatorname{convexHull}_{\\mathbb{R}}(\\operatorname{balancedHull}_{\\mathbb{k}}(s)). $$$$

Lean4

theorem absConvexHull_eq_convexHull_balancedHull [SMulCommClass ℝ 𝕜 E] {s : Set E} :
    absConvexHull 𝕜 s = convexHull ℝ (balancedHull 𝕜 s) :=
  le_antisymm
    (absConvexHull_min ((subset_convexHull ℝ s).trans (convexHull_mono (subset_balancedHull 𝕜)))
      ⟨Balanced.convexHull (balancedHull.balanced s), convex_convexHull ..⟩)
    (convexHull_min (balanced_absConvexHull.balancedHull_subset_of_subset subset_absConvexHull) convex_absConvexHull)

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