mem_convexHull_iff — Mathlib

English

An element x is in the convex hull of s iff for every convex set t containing s, x ∈ t.

Русский

Элемент x принадлежит выпуклой оболочке s тогда и только тогда, когда для каждого выпуклого множества t, содержающего s, x ∈ t.

LaTeX

$$$x \\in \\ convexHull_{\\mathbb{K}}(s) \\iff \\forall t, (s \\subseteq t) \\land (Convex 𝕜 t) \\Rightarrow x \\in t$$$

Lean4

theorem mem_convexHull_iff : x ∈ convexHull 𝕜 s ↔ ∀ t, s ⊆ t → Convex 𝕜 t → x ∈ t := by
  simp_rw [convexHull_eq_iInter, mem_iInter]

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