convex_remove_iff_notMem_convexHull_remove

English

The convex hull of convexHull s union convexHull t equals convexHull of s union t.

Русский

Оболочка объединения выпуклой оболочки s и выпуклой оболочки t равна оболочке объединения s и t.

LaTeX

$$$ convexHull 𝕜 (convexHull 𝕜 s \\cup convexHull 𝕜 t) = convexHull 𝕜 (s \\cup t) $$$

Lean4

theorem convex_remove_iff_notMem_convexHull_remove {s : Set E} (hs : Convex 𝕜 s) (x : E) :
    Convex 𝕜 (s \ { x }) ↔ x ∉ convexHull 𝕜 (s \ { x }) :=
  by
  constructor
  · rintro hsx hx
    rw [hsx.convexHull_eq] at hx
    exact hx.2 (mem_singleton _)
  rintro hx
  suffices h : s \ { x } = convexHull 𝕜 (s \ { x }) by
    rw [h]
    exact convex_convexHull 𝕜 _
  exact
    Subset.antisymm (subset_convexHull 𝕜 _) fun y hy =>
      ⟨convexHull_min diff_subset hs hy, by
        rintro (rfl : y = x)
        exact hx hy⟩

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