convexHull_eq_empty — Mathlib

English

The convex hull of s is empty if and only if s is empty.

Русский

Выпуклая оболочка множества равна пустому множеству тогда и только тогда, когда множество пусто.

LaTeX

$$$ convexHull 𝕜 s = \\emptyset \\iff s = \\emptyset $$$

Lean4

@[simp]
theorem convexHull_eq_empty : convexHull 𝕜 s = ∅ ↔ s = ∅ :=
  by
  constructor
  · intro h
    rw [← Set.subset_empty_iff, ← h]
    exact subset_convexHull 𝕜 _
  · rintro rfl
    exact convexHull_empty

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