English
The inner dual cone is a pointed cone; it contains 0 and has no nonzero element with its negative also in the cone.
Русский
Внутренний двойной конус является указываемым: содержит 0 и нет ненулевого элемента, чье отрицательное тоже принадлежит конусу.
LaTeX
$$$\\text{innerDualCone}\\text{ is pointed}$$$
Lean4
/-- The dual cone is the cone consisting of all points `y` such that for
all points `x` in a given set `0 ≤ ⟪ x, y ⟫`. -/
@[deprecated ProperCone.innerDual (since := "2025-07-06")]
def innerDualCone (s : Set H) : ConvexCone ℝ H
where
carrier := {y | ∀ x ∈ s, 0 ≤ ⟪x, y⟫}
smul_mem' c hc y hy x
hx := by
rw [real_inner_smul_right]
exact mul_nonneg hc.le (hy x hx)
add_mem' u hu v hv x
hx := by
rw [inner_add_right]
exact add_nonneg (hu x hx) (hv x hx)
