convexHull — Mathlib

English

If s is balanced, then convexHull is balanced (same as 52300).

Русский

Если s сбалансировано, то convexHull равновесно (то же самое, что и 52300).

LaTeX

$$$\\text{Balanced } 𝕜 s \Rightarrow \\text{Balanced } 𝕜 (convexHull ℝ s)$$$

Lean4

protected theorem convexHull (hs : Balanced 𝕜 s) : Balanced 𝕜 (convexHull ℝ s) :=
  by
  suffices Convex ℝ {x | ∀ a : 𝕜, ‖a‖ ≤ 1 → a • x ∈ convexHull ℝ s}
    by
    rw [balanced_iff_smul_mem] at hs ⊢
    refine fun a ha x hx => convexHull_min ?_ this hx a ha
    exact fun y hy a ha => subset_convexHull ℝ s (hs ha hy)
  intro x hx y hy u v hu hv huv a ha
  simp only [smul_add, ← smul_comm]
  exact convex_convexHull ℝ s (hx a ha) (hy a ha) hu hv huv

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