balancedHull_convexHull_subseteq_absConvexHull

English

The balanced hull of the convex hull of s is contained in the absConvexHull of s.

Русский

Балансированная оболочка выпуклой оболочки множества s содержится в absConvexHull 𝕜 s.

LaTeX

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

Lean4

/-- In general, equality doesn't hold here - e.g. consider `s := {(-1, 1), (1, 1)}` in `ℝ²`. -/
theorem balancedHull_convexHull_subseteq_absConvexHull {s : Set E} :
    balancedHull 𝕜 (convexHull ℝ s) ⊆ absConvexHull 𝕜 s :=
  balanced_absConvexHull.balancedHull_subset_of_subset (convexHull_min subset_absConvexHull convex_absConvexHull)

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