convexHull_nonempty_iff — Mathlib

English

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

Русский

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

LaTeX

$$$ (convexHull 𝕜 s).Nonempty \\iff s.Nonempty $$$

Lean4

@[simp]
theorem convexHull_nonempty_iff : (convexHull 𝕜 s).Nonempty ↔ s.Nonempty :=
  by
  rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne, Ne]
  exact not_congr convexHull_eq_empty

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