convexHull_eq_singleton — Mathlib

English

The convex hull of s equals a singleton {x} if and only if s itself is {x}.

Русский

Выпуклая оболочка s равна одиночке {x} тогда и только тогда, когда s = {x}.

LaTeX

$$$ convexHull 𝕜 s = { x } \\iff s = { x } $$$

Lean4

@[simp]
theorem convexHull_eq_singleton : convexHull 𝕜 s = { x } ↔ s = { x }
    where
  mp
    hs := by
    rw [← Set.Nonempty.subset_singleton_iff, ← hs]
    · exact subset_convexHull ..
    · by_contra! hs
      simp_all [eq_comm (a := ∅)]
  mpr hs := by simp [hs]

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