English
The cone generated by the convex hull of s is the least cone containing s; i.e., the cone of convext hull is minimal.
Русский
Конус, порождаемый выпуклой оболочкой множества, является наименьшим конусом, содержащим множество.
LaTeX
$$IsLeast {t : ConvexCone 𝕜 M | s ⊆ t} ((convex_convexHull 𝕜 s).toCone _)$$
Lean4
/-- The dual cone of a set `s` with respect to a bilinear pairing `p` is the cone consisting of all
points `y` such that for all points `x ∈ s` we have `0 ≤ p x y`. -/
def dual (s : Set M) : PointedCone R N
where
carrier := {y | ∀ ⦃x⦄, x ∈ s → 0 ≤ p x y}
zero_mem' := by simp
add_mem' {u v} hu hv x hx := by rw [map_add]; exact add_nonneg (hu hx) (hv hx)
smul_mem' c y hy x hx := by rw [← Nonneg.coe_smul, map_smul]; exact mul_nonneg c.2 (hy hx)
