convexHull_eq_iInter — Mathlib

English

The convex hull equals the intersection of all convex supersets: convexHull 𝕜 s = ⋂ t, s ⊆ t and Convex 𝕜 t, t.

Русский

Выпуклая оболочка равна пересечению всех выпуклых надмножеств: convexHull 𝕜 s = ⋂ t, где s ⊆ t и Convex 𝕜 t, t.

LaTeX

$$$\\text{convexHull}_{\\mathbb{K}}(s) = \\bigcap_{t:\\ Sets E,\\ s \\subseteq t,\\ Convex 𝕜 t} t$$$

Lean4

theorem convexHull_eq_iInter : convexHull 𝕜 s = ⋂ (t : Set E) (_ : s ⊆ t) (_ : Convex 𝕜 t), t := by
  simp [convexHull, iInter_subtype, iInter_and]

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