convexHull_toCone_eq_sInf — Mathlib

English

The cone generated by the convex hull of s equals the infimum of all cones containing s: convexHull_toCone_eq_sInf.

Русский

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

LaTeX

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

Lean4

theorem convexHull_toCone_eq_sInf (s : Set M) : (convex_convexHull 𝕜 s).toCone _ = sInf {t : ConvexCone 𝕜 M | s ⊆ t} :=
  Eq.symm <| IsGLB.sInf_eq <| IsLeast.isGLB <| convexHull_toCone_isLeast s

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