convexHull_toCone_isLeast — Mathlib

English

The cone generated by the convex hull of s is the least cone containing s; equivalently, convext hull cone is least.

Русский

Конус, порождаемый выпуклой оболочкой s, является наименьшим конусом, содержащим s.

LaTeX

$$IsLeast { t : ConvexCone 𝕜 M | s ⊆ t } ((convex_convexHull 𝕜 s).toCone _)$$

Lean4

theorem convexHull_toCone_isLeast (s : Set M) :
    IsLeast {t : ConvexCone 𝕜 M | s ⊆ t} ((convex_convexHull 𝕜 s).toCone _) :=
  by
  convert (convex_convexHull 𝕜 s).toCone_isLeast using 1
  ext t
  exact ⟨fun h => convexHull_min h t.convex, (subset_convexHull 𝕜 s).trans⟩

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