English
For any subset s of a real vector space E, the balanced hull of s is contained in the convex hull of s ∪ (−s).
Русский
Для любого подмножества s в векторном пространстве E над ℝ сбалансированная оболочка s ⊆ выпуклая оболочка (s ∪ (−s)).
LaTeX
$$$\\operatorname{balancedHull}_{\\mathbb{R}}(s) \\subseteq \\operatorname{convexHull}_{\\mathbb{R}}(s \\cup (-s))$$$
Lean4
theorem balancedHull_subset_convexHull_union_neg {s : Set E} : balancedHull ℝ s ⊆ convexHull ℝ (s ∪ -s) :=
by
intro a ha
obtain ⟨r, hr, y, hy, rfl⟩ := mem_balancedHull_iff.1 ha
apply segment_subset_convexHull (mem_union_left (-s) hy) (mem_union_right _ (neg_mem_neg.mpr hy))
have : 0 ≤ 1 + r := neg_le_iff_add_nonneg'.mp (neg_le_of_abs_le hr)
have : 0 ≤ 1 - r := sub_nonneg.2 (le_of_abs_le hr)
refine ⟨(1 + r) / 2, (1 - r) / 2, by positivity, by positivity, by ring, ?_⟩
rw [smul_neg, ← sub_eq_add_neg, ← sub_smul]
apply congrFun (congrArg HSMul.hSMul _) y
ring_nf
