absConvexHull_eq_empty — Mathlib

English

absConvexHull 𝕜 s = ∅ iff s = ∅.

Русский

absConvexHull 𝕜 s = ∅ тогда и только тогда, когда s = ∅.

LaTeX

$$$$ \\operatorname{absConvexHull}_{\\mathbb{k}}(s) = \\emptyset \\iff s = \\emptyset. $$$$

Lean4

@[simp]
theorem absConvexHull_eq_empty : absConvexHull 𝕜 s = ∅ ↔ s = ∅ :=
  by
  constructor
  · intro h
    rw [← Set.subset_empty_iff, ← h]
    exact subset_absConvexHull
  · rintro rfl
    exact absConvexHull_empty

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