pointed_innerDualCone — Mathlib

English

The inner dual cone of a singleton {x} is the preimage of the nonnegative reals under the map y ↦ ⟪x,y⟫.

Русский

Двойной конус одиночного вектора {x} — прообраз неотрицательных вещественных чисел под отображением y ↦ ⟪x,y⟫.

LaTeX

$$$\\text{innerDual}({x}) = (\\mathbb{R}_{\\ge 0})\\text{ comap } (\\langle x, \\cdot \\rangle)$$$

Lean4

@[deprecated ProperCone.pointed_toConvexCone (since := "2025-07-06")]
theorem pointed_innerDualCone : s.innerDualCone.Pointed := fun x _ => by rw [inner_zero_right]

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